Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldgenpisyslem1 Structured version   Visualization version   GIF version

Theorem ldgenpisyslem1 32762
Description: Lemma for ldgenpisys 32765. (Contributed by Thierry Arnoux, 29-Jun-2020.)
Hypotheses
Ref Expression
dynkin.p 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}
dynkin.l 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
dynkin.o (𝜑𝑂𝑉)
ldgenpisys.e 𝐸 = {𝑡𝐿𝑇𝑡}
ldgenpisys.1 (𝜑𝑇𝑃)
ldgenpisyslem1.1 (𝜑𝐴𝐸)
Assertion
Ref Expression
ldgenpisyslem1 (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝐿)
Distinct variable groups:   𝑡,𝑠,𝑥,𝑦,𝐿   𝑂,𝑠,𝑡,𝑥   𝑡,𝑃,𝑥,𝑦   𝐿,𝑠   𝑇,𝑠,𝑡,𝑥   𝜑,𝑡,𝑥   𝑠,𝑏,𝑥,𝐴,𝑡,𝑦   𝐸,𝑏,𝑠,𝑡,𝑥,𝑦   𝑂,𝑏,𝑦   𝑥,𝑉   𝑦,𝑇   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑠,𝑏)   𝑃(𝑠,𝑏)   𝑇(𝑏)   𝐿(𝑏)   𝑉(𝑦,𝑡,𝑠,𝑏)

Proof of Theorem ldgenpisyslem1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ssrab2 4037 . . 3 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂
2 dynkin.o . . . 4 (𝜑𝑂𝑉)
3 pwexg 5333 . . . 4 (𝑂𝑉 → 𝒫 𝑂 ∈ V)
4 rabexg 5288 . . . 4 (𝒫 𝑂 ∈ V → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ V)
5 elpwg 4563 . . . 4 ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ V → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂))
62, 3, 4, 54syl 19 . . 3 (𝜑 → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂))
71, 6mpbiri 257 . 2 (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂)
8 ineq2 4166 . . . . 5 (𝑏 = ∅ → (𝐴𝑏) = (𝐴 ∩ ∅))
98eleq1d 2822 . . . 4 (𝑏 = ∅ → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 ∩ ∅) ∈ 𝐸))
10 0elpw 5311 . . . . 5 ∅ ∈ 𝒫 𝑂
1110a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝑂)
12 dynkin.l . . . . . . . . . . . 12 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
1312isldsys 32755 . . . . . . . . . . 11 (𝑡𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1413simprbi 497 . . . . . . . . . 10 (𝑡𝐿 → (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)))
1514simp1d 1142 . . . . . . . . 9 (𝑡𝐿 → ∅ ∈ 𝑡)
1615ad2antlr 725 . . . . . . . 8 (((𝜑𝑡𝐿) ∧ 𝑇𝑡) → ∅ ∈ 𝑡)
1716ex 413 . . . . . . 7 ((𝜑𝑡𝐿) → (𝑇𝑡 → ∅ ∈ 𝑡))
1817ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑡𝐿 (𝑇𝑡 → ∅ ∈ 𝑡))
19 0ex 5264 . . . . . . 7 ∅ ∈ V
2019elintrab 4921 . . . . . 6 (∅ ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → ∅ ∈ 𝑡))
2118, 20sylibr 233 . . . . 5 (𝜑 → ∅ ∈ {𝑡𝐿𝑇𝑡})
22 in0 4351 . . . . 5 (𝐴 ∩ ∅) = ∅
23 ldgenpisys.e . . . . 5 𝐸 = {𝑡𝐿𝑇𝑡}
2421, 22, 233eltr4g 2855 . . . 4 (𝜑 → (𝐴 ∩ ∅) ∈ 𝐸)
259, 11, 24elrabd 3647 . . 3 (𝜑 → ∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
26 ineq2 4166 . . . . . . . 8 (𝑏 = 𝑥 → (𝐴𝑏) = (𝐴𝑥))
2726eleq1d 2822 . . . . . . 7 (𝑏 = 𝑥 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴𝑥) ∈ 𝐸))
2827elrab 3645 . . . . . 6 (𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸))
29 pwidg 4580 . . . . . . . . . 10 (𝑂𝑉𝑂 ∈ 𝒫 𝑂)
302, 29syl 17 . . . . . . . . 9 (𝜑𝑂 ∈ 𝒫 𝑂)
3130adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → 𝑂 ∈ 𝒫 𝑂)
3231elpwdifcl 31454 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝑂𝑥) ∈ 𝒫 𝑂)
3312pwldsys 32756 . . . . . . . . . . . . . . . . . . 19 (𝑂𝑉 → 𝒫 𝑂𝐿)
342, 33syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝒫 𝑂𝐿)
35 ldgenpisys.1 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇𝑃)
36 dynkin.p . . . . . . . . . . . . . . . . . . . . . 22 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}
3736ispisys 32751 . . . . . . . . . . . . . . . . . . . . 21 (𝑇𝑃 ↔ (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇))
3835, 37sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇))
3938simpld 495 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ 𝒫 𝒫 𝑂)
4039elpwid 4569 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ 𝒫 𝑂)
41 sseq2 3970 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝒫 𝑂 → (𝑇𝑡𝑇 ⊆ 𝒫 𝑂))
4241intminss 4935 . . . . . . . . . . . . . . . . . 18 ((𝒫 𝑂𝐿𝑇 ⊆ 𝒫 𝑂) → {𝑡𝐿𝑇𝑡} ⊆ 𝒫 𝑂)
4334, 40, 42syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 {𝑡𝐿𝑇𝑡} ⊆ 𝒫 𝑂)
4423, 43eqsstrid 3992 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ⊆ 𝒫 𝑂)
45 ldgenpisyslem1.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴𝐸)
4644, 45sseldd 3945 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ 𝒫 𝑂)
4746elpwid 4569 . . . . . . . . . . . . . 14 (𝜑𝐴𝑂)
4847ad3antrrr 728 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑂)
49 difin 4221 . . . . . . . . . . . . . . . 16 (𝐴 ∖ (𝐴𝑥)) = (𝐴𝑥)
50 difin2 4251 . . . . . . . . . . . . . . . 16 (𝐴𝑂 → (𝐴𝑥) = ((𝑂𝑥) ∩ 𝐴))
5149, 50eqtrid 2788 . . . . . . . . . . . . . . 15 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = ((𝑂𝑥) ∩ 𝐴))
52 incom 4161 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∩ 𝐴) = (𝐴 ∩ (𝑂𝑥))
5351, 52eqtrdi 2792 . . . . . . . . . . . . . 14 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = (𝐴 ∩ (𝑂𝑥)))
54 difuncomp 31472 . . . . . . . . . . . . . 14 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5553, 54eqtr3d 2778 . . . . . . . . . . . . 13 (𝐴𝑂 → (𝐴 ∩ (𝑂𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5648, 55syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 ∩ (𝑂𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
57 difeq2 4076 . . . . . . . . . . . . . 14 (𝑦 = ((𝑂𝐴) ∪ (𝐴𝑥)) → (𝑂𝑦) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5857eleq1d 2822 . . . . . . . . . . . . 13 (𝑦 = ((𝑂𝐴) ∪ (𝐴𝑥)) → ((𝑂𝑦) ∈ 𝑡 ↔ (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))) ∈ 𝑡))
5914simp2d 1143 . . . . . . . . . . . . . . 15 (𝑡𝐿 → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
6059ad2antlr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
61 difeq2 4076 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑂𝑥) = (𝑂𝑦))
6261eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂𝑦) ∈ 𝑡))
6362cbvralvw 3225 . . . . . . . . . . . . . 14 (∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ↔ ∀𝑦𝑡 (𝑂𝑦) ∈ 𝑡)
6460, 63sylib 217 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑦𝑡 (𝑂𝑦) ∈ 𝑡)
65 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑡𝐿)
6645, 23eleqtrdi 2848 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 {𝑡𝐿𝑇𝑡})
67 elintrabg 4922 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐸 → (𝐴 {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡𝐴𝑡)))
6845, 67syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡𝐴𝑡)))
6966, 68mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑡𝐿 (𝑇𝑡𝐴𝑡))
7069r19.21bi 3234 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝐿) → (𝑇𝑡𝐴𝑡))
7170imp 407 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑡)
7271adantllr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑡)
73 difeq2 4076 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐴 → (𝑂𝑥) = (𝑂𝐴))
7473eleq1d 2822 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂𝐴) ∈ 𝑡))
7559adantr 481 . . . . . . . . . . . . . . . 16 ((𝑡𝐿𝐴𝑡) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
76 simpr 485 . . . . . . . . . . . . . . . 16 ((𝑡𝐿𝐴𝑡) → 𝐴𝑡)
7774, 75, 76rspcdva 3582 . . . . . . . . . . . . . . 15 ((𝑡𝐿𝐴𝑡) → (𝑂𝐴) ∈ 𝑡)
7865, 72, 77syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑂𝐴) ∈ 𝑡)
79 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸))
8079simprd 496 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝐸)
8180, 23eleqtrdi 2848 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡})
82 vex 3449 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
8382inex2 5275 . . . . . . . . . . . . . . . . 17 (𝐴𝑥) ∈ V
84 elintrabg 4922 . . . . . . . . . . . . . . . . 17 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡)))
8583, 84mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡)))
8681, 85mpbid 231 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡))
87 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑇𝑡)
88 rspa 3231 . . . . . . . . . . . . . . . 16 ((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡))
8988imp 407 . . . . . . . . . . . . . . 15 (((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝑡)
9086, 65, 87, 89syl21anc 836 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝑡)
91 incom 4161 . . . . . . . . . . . . . . . 16 ((𝑂𝐴) ∩ (𝐴𝑥)) = ((𝐴𝑥) ∩ (𝑂𝐴))
92 inss1 4188 . . . . . . . . . . . . . . . . 17 (𝐴𝑥) ⊆ 𝐴
93 disjdif 4431 . . . . . . . . . . . . . . . . 17 (𝐴 ∩ (𝑂𝐴)) = ∅
94 ssdisj 4419 . . . . . . . . . . . . . . . . 17 (((𝐴𝑥) ⊆ 𝐴 ∧ (𝐴 ∩ (𝑂𝐴)) = ∅) → ((𝐴𝑥) ∩ (𝑂𝐴)) = ∅)
9592, 93, 94mp2an 690 . . . . . . . . . . . . . . . 16 ((𝐴𝑥) ∩ (𝑂𝐴)) = ∅
9691, 95eqtri 2764 . . . . . . . . . . . . . . 15 ((𝑂𝐴) ∩ (𝐴𝑥)) = ∅
9796a1i 11 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝑂𝐴) ∩ (𝐴𝑥)) = ∅)
9812, 65, 78, 90, 97unelldsys 32757 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝑂𝐴) ∪ (𝐴𝑥)) ∈ 𝑡)
9958, 64, 98rspcdva 3582 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))) ∈ 𝑡)
10056, 99eqeltrd 2838 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)
101100ex 413 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡))
102101ralrimiva 3143 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡))
103 inex1g 5276 . . . . . . . . . . . 12 (𝐴𝐸 → (𝐴 ∩ (𝑂𝑥)) ∈ V)
10445, 103syl 17 . . . . . . . . . . 11 (𝜑 → (𝐴 ∩ (𝑂𝑥)) ∈ V)
105104adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ V)
106 elintrabg 4922 . . . . . . . . . 10 ((𝐴 ∩ (𝑂𝑥)) ∈ V → ((𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)))
107105, 106syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ((𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)))
108102, 107mpbird 256 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡})
109108, 23eleqtrrdi 2849 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸)
11032, 109jca 512 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
11128, 110sylan2b 594 . . . . 5 ((𝜑𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
112 ineq2 4166 . . . . . . 7 (𝑏 = (𝑂𝑥) → (𝐴𝑏) = (𝐴 ∩ (𝑂𝑥)))
113112eleq1d 2822 . . . . . 6 (𝑏 = (𝑂𝑥) → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
114113elrab 3645 . . . . 5 ((𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
115111, 114sylibr 233 . . . 4 ((𝜑𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
116115ralrimiva 3143 . . 3 (𝜑 → ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
117 ineq2 4166 . . . . . . 7 (𝑏 = 𝑥 → (𝐴𝑏) = (𝐴 𝑥))
118117eleq1d 2822 . . . . . 6 (𝑏 = 𝑥 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 𝑥) ∈ 𝐸))
1191sspwi 4572 . . . . . . . 8 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝒫 𝑂
120 simplr 767 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
121119, 120sselid 3942 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝒫 𝑂)
122121elpwunicl 31473 . . . . . 6 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑂)
123 uniin2 31471 . . . . . . . . . . . 12 𝑦𝑥 (𝐴𝑦) = (𝐴 𝑥)
124 vex 3449 . . . . . . . . . . . . . 14 𝑦 ∈ V
125124inex2 5275 . . . . . . . . . . . . 13 (𝐴𝑦) ∈ V
126125dfiun3 5921 . . . . . . . . . . . 12 𝑦𝑥 (𝐴𝑦) = ran (𝑦𝑥 ↦ (𝐴𝑦))
127123, 126eqtr3i 2766 . . . . . . . . . . 11 (𝐴 𝑥) = ran (𝑦𝑥 ↦ (𝐴𝑦))
128 simplr 767 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑡𝐿)
129 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑦(𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
130 nfv 1917 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑥 ≼ ω
131 nfdisj1 5084 . . . . . . . . . . . . . . . . . . 19 𝑦Disj 𝑦𝑥 𝑦
132130, 131nfan 1902 . . . . . . . . . . . . . . . . . 18 𝑦(𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
133129, 132nfan 1902 . . . . . . . . . . . . . . . . 17 𝑦((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
134 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑦 𝑡𝐿
135133, 134nfan 1902 . . . . . . . . . . . . . . . 16 𝑦(((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿)
136 nfv 1917 . . . . . . . . . . . . . . . 16 𝑦 𝑇𝑡
137135, 136nfan 1902 . . . . . . . . . . . . . . 15 𝑦((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡)
138 elpwi 4567 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
139138ad4antlr 731 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
140139sselda 3944 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
141 ineq2 4166 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑦 → (𝐴𝑏) = (𝐴𝑦))
142141eleq1d 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑦 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴𝑦) ∈ 𝐸))
143142elrab 3645 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ (𝑦 ∈ 𝒫 𝑂 ∧ (𝐴𝑦) ∈ 𝐸))
144143simprbi 497 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} → (𝐴𝑦) ∈ 𝐸)
145140, 144syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → (𝐴𝑦) ∈ 𝐸)
146 simpllr 774 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑡𝐿)
147 simplr 767 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑇𝑡)
14823eleq2i 2829 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑦) ∈ 𝐸 ↔ (𝐴𝑦) ∈ {𝑡𝐿𝑇𝑡})
149125elintrab 4921 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑦) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
150148, 149bitri 274 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑦) ∈ 𝐸 ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
151 rspa 3231 . . . . . . . . . . . . . . . . . . 19 ((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
152150, 151sylanb 581 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ∈ 𝐸𝑡𝐿) → (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
153152imp 407 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑦) ∈ 𝐸𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑦) ∈ 𝑡)
154145, 146, 147, 153syl21anc 836 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → (𝐴𝑦) ∈ 𝑡)
155154ex 413 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑦𝑥 → (𝐴𝑦) ∈ 𝑡))
156137, 155ralrimi 3240 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑦𝑥 (𝐴𝑦) ∈ 𝑡)
157 eqid 2736 . . . . . . . . . . . . . . 15 (𝑦𝑥 ↦ (𝐴𝑦)) = (𝑦𝑥 ↦ (𝐴𝑦))
158157rnmptss 7070 . . . . . . . . . . . . . 14 (∀𝑦𝑥 (𝐴𝑦) ∈ 𝑡 → ran (𝑦𝑥 ↦ (𝐴𝑦)) ⊆ 𝑡)
159156, 158syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ⊆ 𝑡)
160128, 159sselpwd 5283 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡)
161 simpllr 774 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
162161simpld 495 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑥 ≼ ω)
163 1stcrestlem 22803 . . . . . . . . . . . . 13 (𝑥 ≼ ω → ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω)
164162, 163syl 17 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω)
165161simprd 496 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑦𝑥 𝑦)
166 disjin2 31505 . . . . . . . . . . . . . 14 (Disj 𝑦𝑥 𝑦Disj 𝑦𝑥 (𝐴𝑦))
167 disjrnmpt 31503 . . . . . . . . . . . . . 14 (Disj 𝑦𝑥 (𝐴𝑦) → Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
168165, 166, 1673syl 18 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
169 nfmpt1 5213 . . . . . . . . . . . . . . 15 𝑦(𝑦𝑥 ↦ (𝐴𝑦))
170169nfrn 5907 . . . . . . . . . . . . . 14 𝑦ran (𝑦𝑥 ↦ (𝐴𝑦))
171 nfcv 2907 . . . . . . . . . . . . . 14 𝑧𝑦
172 nfcv 2907 . . . . . . . . . . . . . 14 𝑦𝑧
173 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑧𝑦 = 𝑧)
174170, 171, 172, 173cbvdisjf 31489 . . . . . . . . . . . . 13 (Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
175168, 174sylibr 233 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)
176 breq1 5108 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (𝑧 ≼ ω ↔ ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω))
177172, 170disjeq1f 31491 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (Disj 𝑦𝑧 𝑦Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦))
178176, 177anbi12d 631 . . . . . . . . . . . . . . 15 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → ((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) ↔ (ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)))
179 unieq 4876 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → 𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)))
180179eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → ( 𝑧𝑡 ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡))
181178, 180imbi12d 344 . . . . . . . . . . . . . 14 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡) ↔ ((ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)))
18214simp3d 1144 . . . . . . . . . . . . . . . 16 (𝑡𝐿 → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
183 breq1 5108 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (𝑥 ≼ ω ↔ 𝑧 ≼ ω))
184 disjeq1 5077 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (Disj 𝑦𝑥 𝑦Disj 𝑦𝑧 𝑦))
185183, 184anbi12d 631 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) ↔ (𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦)))
186 unieq 4876 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 𝑥 = 𝑧)
187186eleq1d 2822 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ( 𝑥𝑡 𝑧𝑡))
188185, 187imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡)))
189188cbvralvw 3225 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
190182, 189sylib 217 . . . . . . . . . . . . . . 15 (𝑡𝐿 → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
191190adantr 481 . . . . . . . . . . . . . 14 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
192 simpr 485 . . . . . . . . . . . . . 14 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡)
193181, 191, 192rspcdva 3582 . . . . . . . . . . . . 13 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ((ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡))
194193imp 407 . . . . . . . . . . . 12 (((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) ∧ (ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)
195128, 160, 164, 175, 194syl22anc 837 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)
196127, 195eqeltrid 2842 . . . . . . . . . 10 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 𝑥) ∈ 𝑡)
197196ex 413 . . . . . . . . 9 ((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
198197ralrimiva 3143 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
199 vuniex 7676 . . . . . . . . . 10 𝑥 ∈ V
200199inex2 5275 . . . . . . . . 9 (𝐴 𝑥) ∈ V
201200elintrab 4921 . . . . . . . 8 ((𝐴 𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
202198, 201sylibr 233 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝐴 𝑥) ∈ {𝑡𝐿𝑇𝑡})
203202, 23eleqtrrdi 2849 . . . . . 6 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝐴 𝑥) ∈ 𝐸)
204118, 122, 203elrabd 3647 . . . . 5 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
205204ex 413 . . . 4 ((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))
206205ralrimiva 3143 . . 3 (𝜑 → ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))
20725, 116, 2063jca 1128 . 2 (𝜑 → (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})))
20812isldsys 32755 . 2 ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝐿 ↔ ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))))
2097, 207, 208sylanbrc 583 1 (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝐿)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  {crab 3407  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560   cuni 4865   cint 4907   ciun 4954  Disj wdisj 5070   class class class wbr 5105  cmpt 5188  ran crn 5634  cfv 6496  ωcom 7802  cdom 8881  ficfi 9346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-dju 9837  df-card 9875  df-acn 9878
This theorem is referenced by:  ldgenpisyslem2  32763
  Copyright terms: Public domain W3C validator