Antichain.union_L'_eq_union_I_p

lemma union_L'_eq_union_I_p : ⋃ (L ∈ 𝓛' 𝔄 ϑ N), L = ⋃ (p ∈ 𝔄' 𝔄 ϑ N), (𝓘 (p : 𝔓 X) : Set X) := by  classical  rw [← union_L_eq_union_I_p]  apply le_antisymm  · simpa using! fun _ hL ↦ subset_biUnion_of_mem hL.1  intro x hx  simp only [mem_iUnion, exists_prop] at hx ⊢  obtain ⟨L, hL, hLx⟩ := hx  obtain ⟨M, lM, maxM⟩ := (𝓛 𝔄 ϑ N).toFinset.exists_le_maximal (mem_toFinset.mpr hL)  refine ⟨M, ?_, lM.1 hLx⟩  constructor  · exact mem_toFinset.mp maxM.1  · intro y hy hy'    exact maxM.2 (mem_toFinset.mpr hy) hy'