Metamath Proof Explorer

Theorem ldgenpisyslem1

Description: Lemma for ldgenpisys . (Contributed by Thierry Arnoux, 29-Jun-2020)

Ref Expression
Hypotheses dynkin.p ⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
dynkin.l ⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
dynkin.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
ldgenpisys.e ⊢ 𝐸 = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
ldgenpisys.1 ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
ldgenpisyslem1.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
Assertion ldgenpisyslem1 ( 𝜑 → { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝐿 )

Proof

Step Hyp Ref Expression
1 dynkin.p ⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2 dynkin.l ⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
3 dynkin.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
4 ldgenpisys.e ⊢ 𝐸 = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
5 ldgenpisys.1 ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
6 ldgenpisyslem1.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
7 ssrab2 ⊢ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ⊆ 𝒫 𝑂
8 pwexg ⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V )
9 rabexg ⊢ ( 𝒫 𝑂 ∈ V → { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ V )
10 elpwg ⊢ ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ V → ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝒫 𝒫 𝑂 ↔ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ⊆ 𝒫 𝑂 ) )
11 3 8 9 10 4syl ⊢ ( 𝜑 → ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝒫 𝒫 𝑂 ↔ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ⊆ 𝒫 𝑂 ) )
12 7 11 mpbiri ⊢ ( 𝜑 → { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝒫 𝒫 𝑂 )
13 ineq2 ⊢ ( 𝑏 = ∅ → ( 𝐴 ∩ 𝑏 ) = ( 𝐴 ∩ ∅ ) )
14 13 eleq1d ⊢ ( 𝑏 = ∅ → ( ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 ↔ ( 𝐴 ∩ ∅ ) ∈ 𝐸 ) )
15 0elpw ⊢ ∅ ∈ 𝒫 𝑂
16 15 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 𝑂 )
17 2 isldsys ⊢ ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
18 17 simprbi ⊢ ( 𝑡 ∈ 𝐿 → ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) )
19 18 simp1d ⊢ ( 𝑡 ∈ 𝐿 → ∅ ∈ 𝑡 )
20 19 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ∅ ∈ 𝑡 )
21 20 ex ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( 𝑇 ⊆ 𝑡 → ∅ ∈ 𝑡 ) )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ∅ ∈ 𝑡 ) )
23 0ex ⊢ ∅ ∈ V
24 23 elintrab ⊢ ( ∅ ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ∅ ∈ 𝑡 ) )
25 22 24 sylibr ⊢ ( 𝜑 → ∅ ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } )
26 in0 ⊢ ( 𝐴 ∩ ∅ ) = ∅
27 25 26 4 3eltr4g ⊢ ( 𝜑 → ( 𝐴 ∩ ∅ ) ∈ 𝐸 )
28 14 16 27 elrabd ⊢ ( 𝜑 → ∅ ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
29 ineq2 ⊢ ( 𝑏 = 𝑥 → ( 𝐴 ∩ 𝑏 ) = ( 𝐴 ∩ 𝑥 ) )
30 29 eleq1d ⊢ ( 𝑏 = 𝑥 → ( ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 ↔ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) )
31 30 elrab ⊢ ( 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ↔ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) )
32 pwidg ⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂 )
33 3 32 syl ⊢ ( 𝜑 → 𝑂 ∈ 𝒫 𝑂 )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → 𝑂 ∈ 𝒫 𝑂 )
35 34 elpwdifcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 )
36 2 pwldsys ⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿 )
37 3 36 syl ⊢ ( 𝜑 → 𝒫 𝑂 ∈ 𝐿 )
38 1 ispisys ⊢ ( 𝑇 ∈ 𝑃 ↔ ( 𝑇 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑇 ) ⊆ 𝑇 ) )
39 5 38 sylib ⊢ ( 𝜑 → ( 𝑇 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑇 ) ⊆ 𝑇 ) )
40 39 simpld ⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝒫 𝑂 )
41 40 elpwid ⊢ ( 𝜑 → 𝑇 ⊆ 𝒫 𝑂 )
42 sseq2 ⊢ ( 𝑡 = 𝒫 𝑂 → ( 𝑇 ⊆ 𝑡 ↔ 𝑇 ⊆ 𝒫 𝑂 ) )
43 42 intminss ⊢ ( ( 𝒫 𝑂 ∈ 𝐿 ∧ 𝑇 ⊆ 𝒫 𝑂 ) → ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ⊆ 𝒫 𝑂 )
44 37 41 43 syl2anc ⊢ ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ⊆ 𝒫 𝑂 )
45 4 44 eqsstrid ⊢ ( 𝜑 → 𝐸 ⊆ 𝒫 𝑂 )
46 45 6 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝑂 )
47 46 elpwid ⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
48 47 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝐴 ⊆ 𝑂 )
49 difin ⊢ ( 𝐴 ∖ ( 𝐴 ∩ 𝑥 ) ) = ( 𝐴 ∖ 𝑥 )
50 difin2 ⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∖ 𝑥 ) = ( ( 𝑂 ∖ 𝑥 ) ∩ 𝐴 ) )
51 49 50 eqtrid ⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∖ ( 𝐴 ∩ 𝑥 ) ) = ( ( 𝑂 ∖ 𝑥 ) ∩ 𝐴 ) )
52 incom ⊢ ( ( 𝑂 ∖ 𝑥 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) )
53 51 52 eqtrdi ⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∖ ( 𝐴 ∩ 𝑥 ) ) = ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) )
54 difuncomp ⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∖ ( 𝐴 ∩ 𝑥 ) ) = ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) ) )
55 53 54 eqtr3d ⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) = ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) ) )
56 48 55 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) = ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) ) )
57 difeq2 ⊢ ( 𝑦 = ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) → ( 𝑂 ∖ 𝑦 ) = ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) ) )
58 57 eleq1d ⊢ ( 𝑦 = ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) → ( ( 𝑂 ∖ 𝑦 ) ∈ 𝑡 ↔ ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) ) ∈ 𝑡 ) )
59 18 simp2d ⊢ ( 𝑡 ∈ 𝐿 → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
60 59 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
61 difeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ 𝑦 ) )
62 61 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ↔ ( 𝑂 ∖ 𝑦 ) ∈ 𝑡 ) )
63 62 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ↔ ∀ 𝑦 ∈ 𝑡 ( 𝑂 ∖ 𝑦 ) ∈ 𝑡 )
64 60 63 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ∀ 𝑦 ∈ 𝑡 ( 𝑂 ∖ 𝑦 ) ∈ 𝑡 )
65 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 )
66 6 4 eleqtrdi ⊢ ( 𝜑 → 𝐴 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } )
67 elintrabg ⊢ ( 𝐴 ∈ 𝐸 → ( 𝐴 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡 ) ) )
68 6 67 syl ⊢ ( 𝜑 → ( 𝐴 ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡 ) ) )
69 66 68 mpbid ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡 ) )
70 69 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) → ( 𝑇 ⊆ 𝑡 → 𝐴 ∈ 𝑡 ) )
71 70 imp ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝐴 ∈ 𝑡 )
72 71 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝐴 ∈ 𝑡 )
73 difeq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ 𝐴 ) )
74 73 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ↔ ( 𝑂 ∖ 𝐴 ) ∈ 𝑡 ) )
75 59 adantr ⊢ ( ( 𝑡 ∈ 𝐿 ∧ 𝐴 ∈ 𝑡 ) → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
76 simpr ⊢ ( ( 𝑡 ∈ 𝐿 ∧ 𝐴 ∈ 𝑡 ) → 𝐴 ∈ 𝑡 )
77 74 75 76 rspcdva ⊢ ( ( 𝑡 ∈ 𝐿 ∧ 𝐴 ∈ 𝑡 ) → ( 𝑂 ∖ 𝐴 ) ∈ 𝑡 )
78 65 72 77 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝑂 ∖ 𝐴 ) ∈ 𝑡 )
79 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) )
80 79 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 )
81 80 4 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } )
82 vex ⊢ 𝑥 ∈ V
83 82 inex2 ⊢ ( 𝐴 ∩ 𝑥 ) ∈ V
84 elintrabg ⊢ ( ( 𝐴 ∩ 𝑥 ) ∈ V → ( ( 𝐴 ∩ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 ) ) )
85 83 84 mp1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( ( 𝐴 ∩ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 ) ) )
86 81 85 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 ) )
87 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝑇 ⊆ 𝑡 )
88 rspa ⊢ ( ( ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 ) )
89 88 imp ⊢ ( ( ( ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 )
90 86 65 87 89 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ 𝑥 ) ∈ 𝑡 )
91 incom ⊢ ( ( 𝑂 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝑥 ) ) = ( ( 𝐴 ∩ 𝑥 ) ∩ ( 𝑂 ∖ 𝐴 ) )
92 inss1 ⊢ ( 𝐴 ∩ 𝑥 ) ⊆ 𝐴
93 disjdif ⊢ ( 𝐴 ∩ ( 𝑂 ∖ 𝐴 ) ) = ∅
94 ssdisj ⊢ ( ( ( 𝐴 ∩ 𝑥 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ ( 𝑂 ∖ 𝐴 ) ) = ∅ ) → ( ( 𝐴 ∩ 𝑥 ) ∩ ( 𝑂 ∖ 𝐴 ) ) = ∅ )
95 92 93 94 mp2an ⊢ ( ( 𝐴 ∩ 𝑥 ) ∩ ( 𝑂 ∖ 𝐴 ) ) = ∅
96 91 95 eqtri ⊢ ( ( 𝑂 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝑥 ) ) = ∅
97 96 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( ( 𝑂 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝑥 ) ) = ∅ )
98 2 65 78 90 97 unelldsys ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) ∈ 𝑡 )
99 58 64 98 rspcdva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝑥 ) ) ) ∈ 𝑡 )
100 56 99 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝑡 )
101 100 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝑡 ) )
102 101 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝑡 ) )
103 inex1g ⊢ ( 𝐴 ∈ 𝐸 → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ V )
104 6 103 syl ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ V )
105 104 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ V )
106 elintrabg ⊢ ( ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ V → ( ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝑡 ) ) )
107 105 106 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → ( ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝑡 ) ) )
108 102 107 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } )
109 108 4 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝐸 )
110 35 109 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑥 ) ∈ 𝐸 ) ) → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝐸 ) )
111 31 110 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝐸 ) )
112 ineq2 ⊢ ( 𝑏 = ( 𝑂 ∖ 𝑥 ) → ( 𝐴 ∩ 𝑏 ) = ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) )
113 112 eleq1d ⊢ ( 𝑏 = ( 𝑂 ∖ 𝑥 ) → ( ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 ↔ ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝐸 ) )
114 113 elrab ⊢ ( ( 𝑂 ∖ 𝑥 ) ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ↔ ( ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ ( 𝑂 ∖ 𝑥 ) ) ∈ 𝐸 ) )
115 111 114 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) → ( 𝑂 ∖ 𝑥 ) ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
116 115 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ( 𝑂 ∖ 𝑥 ) ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
117 ineq2 ⊢ ( 𝑏 = ∪ 𝑥 → ( 𝐴 ∩ 𝑏 ) = ( 𝐴 ∩ ∪ 𝑥 ) )
118 117 eleq1d ⊢ ( 𝑏 = ∪ 𝑥 → ( ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 ↔ ( 𝐴 ∩ ∪ 𝑥 ) ∈ 𝐸 ) )
119 7 sspwi ⊢ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ⊆ 𝒫 𝒫 𝑂
120 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
121 119 120 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑥 ∈ 𝒫 𝒫 𝑂 )
122 121 elpwunicl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∪ 𝑥 ∈ 𝒫 𝑂 )
123 uniin2 ⊢ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ ∪ 𝑥 )
124 vex ⊢ 𝑦 ∈ V
125 124 inex2 ⊢ ( 𝐴 ∩ 𝑦 ) ∈ V
126 125 dfiun3 ⊢ ∪ 𝑦 ∈ 𝑥 ( 𝐴 ∩ 𝑦 ) = ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) )
127 123 126 eqtr3i ⊢ ( 𝐴 ∩ ∪ 𝑥 ) = ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) )
128 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 )
129 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
130 nfv ⊢ Ⅎ 𝑦 𝑥 ≼ ω
131 nfdisj1 ⊢ Ⅎ 𝑦 Disj 𝑦 ∈ 𝑥 𝑦
132 130 131 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 )
133 129 132 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
134 nfv ⊢ Ⅎ 𝑦 𝑡 ∈ 𝐿
135 133 134 nfan ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 )
136 nfv ⊢ Ⅎ 𝑦 𝑇 ⊆ 𝑡
137 135 136 nfan ⊢ Ⅎ 𝑦 ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 )
138 elpwi ⊢ ( 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } → 𝑥 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
139 138 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝑥 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
140 139 sselda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
141 ineq2 ⊢ ( 𝑏 = 𝑦 → ( 𝐴 ∩ 𝑏 ) = ( 𝐴 ∩ 𝑦 ) )
142 141 eleq1d ⊢ ( 𝑏 = 𝑦 → ( ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 ↔ ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 ) )
143 142 elrab ⊢ ( 𝑦 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ↔ ( 𝑦 ∈ 𝒫 𝑂 ∧ ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 ) )
144 143 simprbi ⊢ ( 𝑦 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } → ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 )
145 140 144 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 )
146 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑡 ∈ 𝐿 )
147 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑇 ⊆ 𝑡 )
148 4 eleq2i ⊢ ( ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 ↔ ( 𝐴 ∩ 𝑦 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } )
149 125 elintrab ⊢ ( ( 𝐴 ∩ 𝑦 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 ) )
150 148 149 bitri ⊢ ( ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 ) )
151 rspa ⊢ ( ( ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 ) )
152 150 151 sylanb ⊢ ( ( ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 ∧ 𝑡 ∈ 𝐿 ) → ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 ) )
153 152 imp ⊢ ( ( ( ( 𝐴 ∩ 𝑦 ) ∈ 𝐸 ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 )
154 145 146 147 153 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 )
155 154 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝑦 ∈ 𝑥 → ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 ) )
156 137 155 ralrimi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 )
157 eqid ⊢ ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) )
158 157 rnmptss ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ∩ 𝑦 ) ∈ 𝑡 → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ⊆ 𝑡 )
159 156 158 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ⊆ 𝑡 )
160 128 159 sselpwd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝒫 𝑡 )
161 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
162 161 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → 𝑥 ≼ ω )
163 1stcrestlem ⊢ ( 𝑥 ≼ ω → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ≼ ω )
164 162 163 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ≼ ω )
165 161 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → Disj 𝑦 ∈ 𝑥 𝑦 )
166 disjin2 ⊢ ( Disj 𝑦 ∈ 𝑥 𝑦 → Disj 𝑦 ∈ 𝑥 ( 𝐴 ∩ 𝑦 ) )
167 disjrnmpt ⊢ ( Disj 𝑦 ∈ 𝑥 ( 𝐴 ∩ 𝑦 ) → Disj 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑧 )
168 165 166 167 3syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → Disj 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑧 )
169 nfmpt1 ⊢ Ⅎ 𝑦 ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) )
170 169 nfrn ⊢ Ⅎ 𝑦 ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) )
171 nfcv ⊢ Ⅎ 𝑧 𝑦
172 nfcv ⊢ Ⅎ 𝑦 𝑧
173 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
174 170 171 172 173 cbvdisjf ⊢ ( Disj 𝑦 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑦 ↔ Disj 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑧 )
175 168 174 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → Disj 𝑦 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑦 )
176 breq1 ⊢ ( 𝑧 = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) → ( 𝑧 ≼ ω ↔ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ≼ ω ) )
177 172 170 disjeq1f ⊢ ( 𝑧 = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) → ( Disj 𝑦 ∈ 𝑧 𝑦 ↔ Disj 𝑦 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑦 ) )
178 176 177 anbi12d ⊢ ( 𝑧 = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) → ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ↔ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑦 ) ) )
179 unieq ⊢ ( 𝑧 = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) → ∪ 𝑧 = ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) )
180 179 eleq1d ⊢ ( 𝑧 = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) → ( ∪ 𝑧 ∈ 𝑡 ↔ ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝑡 ) )
181 178 180 imbi12d ⊢ ( 𝑧 = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) → ( ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑡 ) ↔ ( ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑦 ) → ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝑡 ) ) )
182 18 simp3d ⊢ ( 𝑡 ∈ 𝐿 → ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
183 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≼ ω ↔ 𝑧 ≼ ω ) )
184 disjeq1 ⊢ ( 𝑥 = 𝑧 → ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ 𝑧 𝑦 ) )
185 183 184 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ↔ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) )
186 unieq ⊢ ( 𝑥 = 𝑧 → ∪ 𝑥 = ∪ 𝑧 )
187 186 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ∪ 𝑥 ∈ 𝑡 ↔ ∪ 𝑧 ∈ 𝑡 ) )
188 185 187 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ↔ ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑡 ) ) )
189 188 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑡 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑡 ) )
190 182 189 sylib ⊢ ( 𝑡 ∈ 𝐿 → ∀ 𝑧 ∈ 𝒫 𝑡 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑡 ) )
191 190 adantr ⊢ ( ( 𝑡 ∈ 𝐿 ∧ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝒫 𝑡 ) → ∀ 𝑧 ∈ 𝒫 𝑡 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑡 ) )
192 simpr ⊢ ( ( 𝑡 ∈ 𝐿 ∧ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝒫 𝑡 ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝒫 𝑡 )
193 181 191 192 rspcdva ⊢ ( ( 𝑡 ∈ 𝐿 ∧ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝒫 𝑡 ) → ( ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑦 ) → ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝑡 ) )
194 193 imp ⊢ ( ( ( 𝑡 ∈ 𝐿 ∧ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝒫 𝑡 ) ∧ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) 𝑦 ) ) → ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝑡 )
195 128 160 164 175 194 syl22anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝐴 ∩ 𝑦 ) ) ∈ 𝑡 )
196 127 195 eqeltrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) ∧ 𝑇 ⊆ 𝑡 ) → ( 𝐴 ∩ ∪ 𝑥 ) ∈ 𝑡 )
197 196 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ∧ 𝑡 ∈ 𝐿 ) → ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ ∪ 𝑥 ) ∈ 𝑡 ) )
198 197 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ ∪ 𝑥 ) ∈ 𝑡 ) )
199 vuniex ⊢ ∪ 𝑥 ∈ V
200 199 inex2 ⊢ ( 𝐴 ∩ ∪ 𝑥 ) ∈ V
201 200 elintrab ⊢ ( ( 𝐴 ∩ ∪ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → ( 𝐴 ∩ ∪ 𝑥 ) ∈ 𝑡 ) )
202 198 201 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝐴 ∩ ∪ 𝑥 ) ∈ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } )
203 202 4 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝐴 ∩ ∪ 𝑥 ) ∈ 𝐸 )
204 118 122 203 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∪ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
205 204 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) )
206 205 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) )
207 28 116 206 3jca ⊢ ( 𝜑 → ( ∅ ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∧ ∀ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ( 𝑂 ∖ 𝑥 ) ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∧ ∀ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ) )
208 2 isldsys ⊢ ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝐿 ↔ ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∧ ∀ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ( 𝑂 ∖ 𝑥 ) ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∧ ∀ 𝑥 ∈ 𝒫 { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) ) ) )
209 12 207 208 sylanbrc ⊢ ( 𝜑 → { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝐿 )