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 32427
Description: Lemma for ldgenpisys 32430. (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 4029 . . 3 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂
2 dynkin.o . . . 4 (𝜑𝑂𝑉)
3 pwexg 5326 . . . 4 (𝑂𝑉 → 𝒫 𝑂 ∈ V)
4 rabexg 5280 . . . 4 (𝒫 𝑂 ∈ V → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ V)
5 elpwg 4555 . . . 4 ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ V → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂))
62, 3, 4, 54syl 19 . . 3 (𝜑 → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂))
71, 6mpbiri 258 . 2 (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂)
8 ineq2 4158 . . . . 5 (𝑏 = ∅ → (𝐴𝑏) = (𝐴 ∩ ∅))
98eleq1d 2822 . . . 4 (𝑏 = ∅ → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 ∩ ∅) ∈ 𝐸))
10 0elpw 5303 . . . . 5 ∅ ∈ 𝒫 𝑂
1110a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝑂)
12 dynkin.l . . . . . . . . . . . 12 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
1312isldsys 32420 . . . . . . . . . . 11 (𝑡𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1413simprbi 498 . . . . . . . . . 10 (𝑡𝐿 → (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)))
1514simp1d 1142 . . . . . . . . 9 (𝑡𝐿 → ∅ ∈ 𝑡)
1615ad2antlr 725 . . . . . . . 8 (((𝜑𝑡𝐿) ∧ 𝑇𝑡) → ∅ ∈ 𝑡)
1716ex 414 . . . . . . 7 ((𝜑𝑡𝐿) → (𝑇𝑡 → ∅ ∈ 𝑡))
1817ralrimiva 3140 . . . . . 6 (𝜑 → ∀𝑡𝐿 (𝑇𝑡 → ∅ ∈ 𝑡))
19 0ex 5256 . . . . . . 7 ∅ ∈ V
2019elintrab 4913 . . . . . 6 (∅ ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → ∅ ∈ 𝑡))
2118, 20sylibr 233 . . . . 5 (𝜑 → ∅ ∈ {𝑡𝐿𝑇𝑡})
22 in0 4343 . . . . 5 (𝐴 ∩ ∅) = ∅
23 ldgenpisys.e . . . . 5 𝐸 = {𝑡𝐿𝑇𝑡}
2421, 22, 233eltr4g 2855 . . . 4 (𝜑 → (𝐴 ∩ ∅) ∈ 𝐸)
259, 11, 24elrabd 3640 . . 3 (𝜑 → ∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
26 ineq2 4158 . . . . . . . 8 (𝑏 = 𝑥 → (𝐴𝑏) = (𝐴𝑥))
2726eleq1d 2822 . . . . . . 7 (𝑏 = 𝑥 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴𝑥) ∈ 𝐸))
2827elrab 3638 . . . . . 6 (𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸))
29 pwidg 4572 . . . . . . . . . 10 (𝑂𝑉𝑂 ∈ 𝒫 𝑂)
302, 29syl 17 . . . . . . . . 9 (𝜑𝑂 ∈ 𝒫 𝑂)
3130adantr 482 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → 𝑂 ∈ 𝒫 𝑂)
3231elpwdifcl 31160 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝑂𝑥) ∈ 𝒫 𝑂)
3312pwldsys 32421 . . . . . . . . . . . . . . . . . . 19 (𝑂𝑉 → 𝒫 𝑂𝐿)
342, 33syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝒫 𝑂𝐿)
35 ldgenpisys.1 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇𝑃)
36 dynkin.p . . . . . . . . . . . . . . . . . . . . . 22 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}
3736ispisys 32416 . . . . . . . . . . . . . . . . . . . . 21 (𝑇𝑃 ↔ (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇))
3835, 37sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇))
3938simpld 496 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ 𝒫 𝒫 𝑂)
4039elpwid 4561 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ 𝒫 𝑂)
41 sseq2 3962 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝒫 𝑂 → (𝑇𝑡𝑇 ⊆ 𝒫 𝑂))
4241intminss 4927 . . . . . . . . . . . . . . . . . 18 ((𝒫 𝑂𝐿𝑇 ⊆ 𝒫 𝑂) → {𝑡𝐿𝑇𝑡} ⊆ 𝒫 𝑂)
4334, 40, 42syl2anc 585 . . . . . . . . . . . . . . . . 17 (𝜑 {𝑡𝐿𝑇𝑡} ⊆ 𝒫 𝑂)
4423, 43eqsstrid 3984 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ⊆ 𝒫 𝑂)
45 ldgenpisyslem1.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴𝐸)
4644, 45sseldd 3937 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ 𝒫 𝑂)
4746elpwid 4561 . . . . . . . . . . . . . 14 (𝜑𝐴𝑂)
4847ad3antrrr 728 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑂)
49 difin 4213 . . . . . . . . . . . . . . . 16 (𝐴 ∖ (𝐴𝑥)) = (𝐴𝑥)
50 difin2 4243 . . . . . . . . . . . . . . . 16 (𝐴𝑂 → (𝐴𝑥) = ((𝑂𝑥) ∩ 𝐴))
5149, 50eqtrid 2789 . . . . . . . . . . . . . . 15 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = ((𝑂𝑥) ∩ 𝐴))
52 incom 4153 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∩ 𝐴) = (𝐴 ∩ (𝑂𝑥))
5351, 52eqtrdi 2793 . . . . . . . . . . . . . 14 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = (𝐴 ∩ (𝑂𝑥)))
54 difuncomp 31178 . . . . . . . . . . . . . 14 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5553, 54eqtr3d 2779 . . . . . . . . . . . . 13 (𝐴𝑂 → (𝐴 ∩ (𝑂𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5648, 55syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 ∩ (𝑂𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
57 difeq2 4068 . . . . . . . . . . . . . 14 (𝑦 = ((𝑂𝐴) ∪ (𝐴𝑥)) → (𝑂𝑦) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5857eleq1d 2822 . . . . . . . . . . . . 13 (𝑦 = ((𝑂𝐴) ∪ (𝐴𝑥)) → ((𝑂𝑦) ∈ 𝑡 ↔ (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))) ∈ 𝑡))
5914simp2d 1143 . . . . . . . . . . . . . . 15 (𝑡𝐿 → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
6059ad2antlr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
61 difeq2 4068 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑂𝑥) = (𝑂𝑦))
6261eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂𝑦) ∈ 𝑡))
6362cbvralvw 3222 . . . . . . . . . . . . . 14 (∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ↔ ∀𝑦𝑡 (𝑂𝑦) ∈ 𝑡)
6460, 63sylib 217 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑦𝑡 (𝑂𝑦) ∈ 𝑡)
65 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑡𝐿)
6645, 23eleqtrdi 2848 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 {𝑡𝐿𝑇𝑡})
67 elintrabg 4914 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐸 → (𝐴 {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡𝐴𝑡)))
6845, 67syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡𝐴𝑡)))
6966, 68mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑡𝐿 (𝑇𝑡𝐴𝑡))
7069r19.21bi 3231 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝐿) → (𝑇𝑡𝐴𝑡))
7170imp 408 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑡)
7271adantllr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑡)
73 difeq2 4068 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐴 → (𝑂𝑥) = (𝑂𝐴))
7473eleq1d 2822 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂𝐴) ∈ 𝑡))
7559adantr 482 . . . . . . . . . . . . . . . 16 ((𝑡𝐿𝐴𝑡) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
76 simpr 486 . . . . . . . . . . . . . . . 16 ((𝑡𝐿𝐴𝑡) → 𝐴𝑡)
7774, 75, 76rspcdva 3575 . . . . . . . . . . . . . . 15 ((𝑡𝐿𝐴𝑡) → (𝑂𝐴) ∈ 𝑡)
7865, 72, 77syl2anc 585 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑂𝐴) ∈ 𝑡)
79 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸))
8079simprd 497 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝐸)
8180, 23eleqtrdi 2848 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡})
82 vex 3446 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
8382inex2 5267 . . . . . . . . . . . . . . . . 17 (𝐴𝑥) ∈ V
84 elintrabg 4914 . . . . . . . . . . . . . . . . 17 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡)))
8583, 84mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡)))
8681, 85mpbid 231 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡))
87 simpr 486 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑇𝑡)
88 rspa 3228 . . . . . . . . . . . . . . . 16 ((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡))
8988imp 408 . . . . . . . . . . . . . . 15 (((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝑡)
9086, 65, 87, 89syl21anc 836 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝑡)
91 incom 4153 . . . . . . . . . . . . . . . 16 ((𝑂𝐴) ∩ (𝐴𝑥)) = ((𝐴𝑥) ∩ (𝑂𝐴))
92 inss1 4180 . . . . . . . . . . . . . . . . 17 (𝐴𝑥) ⊆ 𝐴
93 disjdif 4423 . . . . . . . . . . . . . . . . 17 (𝐴 ∩ (𝑂𝐴)) = ∅
94 ssdisj 4411 . . . . . . . . . . . . . . . . 17 (((𝐴𝑥) ⊆ 𝐴 ∧ (𝐴 ∩ (𝑂𝐴)) = ∅) → ((𝐴𝑥) ∩ (𝑂𝐴)) = ∅)
9592, 93, 94mp2an 690 . . . . . . . . . . . . . . . 16 ((𝐴𝑥) ∩ (𝑂𝐴)) = ∅
9691, 95eqtri 2765 . . . . . . . . . . . . . . 15 ((𝑂𝐴) ∩ (𝐴𝑥)) = ∅
9796a1i 11 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝑂𝐴) ∩ (𝐴𝑥)) = ∅)
9812, 65, 78, 90, 97unelldsys 32422 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝑂𝐴) ∪ (𝐴𝑥)) ∈ 𝑡)
9958, 64, 98rspcdva 3575 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))) ∈ 𝑡)
10056, 99eqeltrd 2838 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)
101100ex 414 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡))
102101ralrimiva 3140 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡))
103 inex1g 5268 . . . . . . . . . . . 12 (𝐴𝐸 → (𝐴 ∩ (𝑂𝑥)) ∈ V)
10445, 103syl 17 . . . . . . . . . . 11 (𝜑 → (𝐴 ∩ (𝑂𝑥)) ∈ V)
105104adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ V)
106 elintrabg 4914 . . . . . . . . . 10 ((𝐴 ∩ (𝑂𝑥)) ∈ V → ((𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)))
107105, 106syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ((𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)))
108102, 107mpbird 257 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡})
109108, 23eleqtrrdi 2849 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸)
11032, 109jca 513 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
11128, 110sylan2b 595 . . . . 5 ((𝜑𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
112 ineq2 4158 . . . . . . 7 (𝑏 = (𝑂𝑥) → (𝐴𝑏) = (𝐴 ∩ (𝑂𝑥)))
113112eleq1d 2822 . . . . . 6 (𝑏 = (𝑂𝑥) → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
114113elrab 3638 . . . . 5 ((𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
115111, 114sylibr 233 . . . 4 ((𝜑𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
116115ralrimiva 3140 . . 3 (𝜑 → ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
117 ineq2 4158 . . . . . . 7 (𝑏 = 𝑥 → (𝐴𝑏) = (𝐴 𝑥))
118117eleq1d 2822 . . . . . 6 (𝑏 = 𝑥 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 𝑥) ∈ 𝐸))
1191sspwi 4564 . . . . . . . 8 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝒫 𝑂
120 simplr 767 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
121119, 120sselid 3934 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝒫 𝑂)
122121elpwunicl 31179 . . . . . 6 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑂)
123 uniin2 31177 . . . . . . . . . . . 12 𝑦𝑥 (𝐴𝑦) = (𝐴 𝑥)
124 vex 3446 . . . . . . . . . . . . . 14 𝑦 ∈ V
125124inex2 5267 . . . . . . . . . . . . 13 (𝐴𝑦) ∈ V
126125dfiun3 5912 . . . . . . . . . . . 12 𝑦𝑥 (𝐴𝑦) = ran (𝑦𝑥 ↦ (𝐴𝑦))
127123, 126eqtr3i 2767 . . . . . . . . . . 11 (𝐴 𝑥) = ran (𝑦𝑥 ↦ (𝐴𝑦))
128 simplr 767 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑡𝐿)
129 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑦(𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
130 nfv 1917 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑥 ≼ ω
131 nfdisj1 5076 . . . . . . . . . . . . . . . . . . 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 4559 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
139138ad4antlr 731 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
140139sselda 3936 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
141 ineq2 4158 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑦 → (𝐴𝑏) = (𝐴𝑦))
142141eleq1d 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑦 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴𝑦) ∈ 𝐸))
143142elrab 3638 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ (𝑦 ∈ 𝒫 𝑂 ∧ (𝐴𝑦) ∈ 𝐸))
144143simprbi 498 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} → (𝐴𝑦) ∈ 𝐸)
145140, 144syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → (𝐴𝑦) ∈ 𝐸)
146 simpllr 774 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑡𝐿)
147 simplr 767 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑇𝑡)
14823eleq2i 2829 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑦) ∈ 𝐸 ↔ (𝐴𝑦) ∈ {𝑡𝐿𝑇𝑡})
149125elintrab 4913 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑦) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
150148, 149bitri 275 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑦) ∈ 𝐸 ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
151 rspa 3228 . . . . . . . . . . . . . . . . . . 19 ((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
152150, 151sylanb 582 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ∈ 𝐸𝑡𝐿) → (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
153152imp 408 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑦) ∈ 𝐸𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑦) ∈ 𝑡)
154145, 146, 147, 153syl21anc 836 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → (𝐴𝑦) ∈ 𝑡)
155154ex 414 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑦𝑥 → (𝐴𝑦) ∈ 𝑡))
156137, 155ralrimi 3237 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑦𝑥 (𝐴𝑦) ∈ 𝑡)
157 eqid 2737 . . . . . . . . . . . . . . 15 (𝑦𝑥 ↦ (𝐴𝑦)) = (𝑦𝑥 ↦ (𝐴𝑦))
158157rnmptss 7057 . . . . . . . . . . . . . 14 (∀𝑦𝑥 (𝐴𝑦) ∈ 𝑡 → ran (𝑦𝑥 ↦ (𝐴𝑦)) ⊆ 𝑡)
159156, 158syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ⊆ 𝑡)
160128, 159sselpwd 5275 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡)
161 simpllr 774 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
162161simpld 496 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑥 ≼ ω)
163 1stcrestlem 22709 . . . . . . . . . . . . 13 (𝑥 ≼ ω → ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω)
164162, 163syl 17 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω)
165161simprd 497 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑦𝑥 𝑦)
166 disjin2 31211 . . . . . . . . . . . . . 14 (Disj 𝑦𝑥 𝑦Disj 𝑦𝑥 (𝐴𝑦))
167 disjrnmpt 31209 . . . . . . . . . . . . . 14 (Disj 𝑦𝑥 (𝐴𝑦) → Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
168165, 166, 1673syl 18 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
169 nfmpt1 5205 . . . . . . . . . . . . . . 15 𝑦(𝑦𝑥 ↦ (𝐴𝑦))
170169nfrn 5898 . . . . . . . . . . . . . 14 𝑦ran (𝑦𝑥 ↦ (𝐴𝑦))
171 nfcv 2905 . . . . . . . . . . . . . 14 𝑧𝑦
172 nfcv 2905 . . . . . . . . . . . . . 14 𝑦𝑧
173 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑧𝑦 = 𝑧)
174170, 171, 172, 173cbvdisjf 31195 . . . . . . . . . . . . 13 (Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
175168, 174sylibr 233 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)
176 breq1 5100 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (𝑧 ≼ ω ↔ ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω))
177172, 170disjeq1f 31197 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (Disj 𝑦𝑧 𝑦Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦))
178176, 177anbi12d 632 . . . . . . . . . . . . . . 15 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → ((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) ↔ (ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)))
179 unieq 4868 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → 𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)))
180179eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → ( 𝑧𝑡 ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡))
181178, 180imbi12d 345 . . . . . . . . . . . . . 14 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡) ↔ ((ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)))
18214simp3d 1144 . . . . . . . . . . . . . . . 16 (𝑡𝐿 → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
183 breq1 5100 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (𝑥 ≼ ω ↔ 𝑧 ≼ ω))
184 disjeq1 5069 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (Disj 𝑦𝑥 𝑦Disj 𝑦𝑧 𝑦))
185183, 184anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) ↔ (𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦)))
186 unieq 4868 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 𝑥 = 𝑧)
187186eleq1d 2822 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ( 𝑥𝑡 𝑧𝑡))
188185, 187imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡)))
189188cbvralvw 3222 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
190182, 189sylib 217 . . . . . . . . . . . . . . 15 (𝑡𝐿 → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
191190adantr 482 . . . . . . . . . . . . . 14 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
192 simpr 486 . . . . . . . . . . . . . 14 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡)
193181, 191, 192rspcdva 3575 . . . . . . . . . . . . 13 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ((ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡))
194193imp 408 . . . . . . . . . . . 12 (((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) ∧ (ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)
195128, 160, 164, 175, 194syl22anc 837 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)
196127, 195eqeltrid 2842 . . . . . . . . . 10 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 𝑥) ∈ 𝑡)
197196ex 414 . . . . . . . . 9 ((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
198197ralrimiva 3140 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
199 vuniex 7659 . . . . . . . . . 10 𝑥 ∈ V
200199inex2 5267 . . . . . . . . 9 (𝐴 𝑥) ∈ V
201200elintrab 4913 . . . . . . . 8 ((𝐴 𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
202198, 201sylibr 233 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝐴 𝑥) ∈ {𝑡𝐿𝑇𝑡})
203202, 23eleqtrrdi 2849 . . . . . 6 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝐴 𝑥) ∈ 𝐸)
204118, 122, 203elrabd 3640 . . . . 5 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
205204ex 414 . . . 4 ((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))
206205ralrimiva 3140 . . 3 (𝜑 → ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))
20725, 116, 2063jca 1128 . 2 (𝜑 → (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})))
20812isldsys 32420 . 2 ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝐿 ↔ ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))))
2097, 207, 208sylanbrc 584 1 (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝐿)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wcel 2106  wral 3062  {crab 3404  Vcvv 3442  cdif 3899  cun 3900  cin 3901  wss 3902  c0 4274  𝒫 cpw 4552   cuni 4857   cint 4899   ciun 4946  Disj wdisj 5062   class class class wbr 5097  cmpt 5180  ran crn 5626  cfv 6484  ωcom 7785  cdom 8807  ficfi 9272
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 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-inf2 9503
This theorem depends on definitions:  df-bi 206  df-an 398  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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-int 4900  df-iun 4948  df-disj 5063  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-se 5581  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-isom 6493  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-om 7786  df-1st 7904  df-2nd 7905  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-1o 8372  df-2o 8373  df-er 8574  df-map 8693  df-en 8810  df-dom 8811  df-sdom 8812  df-fin 8813  df-oi 9372  df-dju 9763  df-card 9801  df-acn 9804
This theorem is referenced by:  ldgenpisyslem2  32428
  Copyright terms: Public domain W3C validator