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 33996
Description: Lemma for ldgenpisys 33999. (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 4076 . . 3 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂
2 dynkin.o . . . 4 (𝜑𝑂𝑉)
3 pwexg 5382 . . . 4 (𝑂𝑉 → 𝒫 𝑂 ∈ V)
4 rabexg 5338 . . . 4 (𝒫 𝑂 ∈ V → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ V)
5 elpwg 4610 . . . 4 ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ V → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂))
62, 3, 4, 54syl 19 . . 3 (𝜑 → ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ↔ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝑂))
71, 6mpbiri 257 . 2 (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂)
8 ineq2 4207 . . . . 5 (𝑏 = ∅ → (𝐴𝑏) = (𝐴 ∩ ∅))
98eleq1d 2811 . . . 4 (𝑏 = ∅ → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 ∩ ∅) ∈ 𝐸))
10 0elpw 5360 . . . . 5 ∅ ∈ 𝒫 𝑂
1110a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 𝑂)
12 dynkin.l . . . . . . . . . . . 12 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
1312isldsys 33989 . . . . . . . . . . 11 (𝑡𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1413simprbi 495 . . . . . . . . . 10 (𝑡𝐿 → (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)))
1514simp1d 1139 . . . . . . . . 9 (𝑡𝐿 → ∅ ∈ 𝑡)
1615ad2antlr 725 . . . . . . . 8 (((𝜑𝑡𝐿) ∧ 𝑇𝑡) → ∅ ∈ 𝑡)
1716ex 411 . . . . . . 7 ((𝜑𝑡𝐿) → (𝑇𝑡 → ∅ ∈ 𝑡))
1817ralrimiva 3136 . . . . . 6 (𝜑 → ∀𝑡𝐿 (𝑇𝑡 → ∅ ∈ 𝑡))
19 0ex 5312 . . . . . . 7 ∅ ∈ V
2019elintrab 4968 . . . . . 6 (∅ ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → ∅ ∈ 𝑡))
2118, 20sylibr 233 . . . . 5 (𝜑 → ∅ ∈ {𝑡𝐿𝑇𝑡})
22 in0 4396 . . . . 5 (𝐴 ∩ ∅) = ∅
23 ldgenpisys.e . . . . 5 𝐸 = {𝑡𝐿𝑇𝑡}
2421, 22, 233eltr4g 2843 . . . 4 (𝜑 → (𝐴 ∩ ∅) ∈ 𝐸)
259, 11, 24elrabd 3683 . . 3 (𝜑 → ∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
26 ineq2 4207 . . . . . . . 8 (𝑏 = 𝑥 → (𝐴𝑏) = (𝐴𝑥))
2726eleq1d 2811 . . . . . . 7 (𝑏 = 𝑥 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴𝑥) ∈ 𝐸))
2827elrab 3681 . . . . . 6 (𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸))
29 pwidg 4627 . . . . . . . . . 10 (𝑂𝑉𝑂 ∈ 𝒫 𝑂)
302, 29syl 17 . . . . . . . . 9 (𝜑𝑂 ∈ 𝒫 𝑂)
3130adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → 𝑂 ∈ 𝒫 𝑂)
3231elpwdifcl 32453 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝑂𝑥) ∈ 𝒫 𝑂)
3312pwldsys 33990 . . . . . . . . . . . . . . . . . . 19 (𝑂𝑉 → 𝒫 𝑂𝐿)
342, 33syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝒫 𝑂𝐿)
35 ldgenpisys.1 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇𝑃)
36 dynkin.p . . . . . . . . . . . . . . . . . . . . . 22 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}
3736ispisys 33985 . . . . . . . . . . . . . . . . . . . . 21 (𝑇𝑃 ↔ (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇))
3835, 37sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑇 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑇) ⊆ 𝑇))
3938simpld 493 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ 𝒫 𝒫 𝑂)
4039elpwid 4616 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ 𝒫 𝑂)
41 sseq2 4006 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝒫 𝑂 → (𝑇𝑡𝑇 ⊆ 𝒫 𝑂))
4241intminss 4982 . . . . . . . . . . . . . . . . . 18 ((𝒫 𝑂𝐿𝑇 ⊆ 𝒫 𝑂) → {𝑡𝐿𝑇𝑡} ⊆ 𝒫 𝑂)
4334, 40, 42syl2anc 582 . . . . . . . . . . . . . . . . 17 (𝜑 {𝑡𝐿𝑇𝑡} ⊆ 𝒫 𝑂)
4423, 43eqsstrid 4028 . . . . . . . . . . . . . . . 16 (𝜑𝐸 ⊆ 𝒫 𝑂)
45 ldgenpisyslem1.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴𝐸)
4644, 45sseldd 3980 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ 𝒫 𝑂)
4746elpwid 4616 . . . . . . . . . . . . . 14 (𝜑𝐴𝑂)
4847ad3antrrr 728 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑂)
49 difin 4263 . . . . . . . . . . . . . . . 16 (𝐴 ∖ (𝐴𝑥)) = (𝐴𝑥)
50 difin2 4293 . . . . . . . . . . . . . . . 16 (𝐴𝑂 → (𝐴𝑥) = ((𝑂𝑥) ∩ 𝐴))
5149, 50eqtrid 2778 . . . . . . . . . . . . . . 15 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = ((𝑂𝑥) ∩ 𝐴))
52 incom 4202 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∩ 𝐴) = (𝐴 ∩ (𝑂𝑥))
5351, 52eqtrdi 2782 . . . . . . . . . . . . . 14 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = (𝐴 ∩ (𝑂𝑥)))
54 difuncomp 32474 . . . . . . . . . . . . . 14 (𝐴𝑂 → (𝐴 ∖ (𝐴𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5553, 54eqtr3d 2768 . . . . . . . . . . . . 13 (𝐴𝑂 → (𝐴 ∩ (𝑂𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5648, 55syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 ∩ (𝑂𝑥)) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
57 difeq2 4115 . . . . . . . . . . . . . 14 (𝑦 = ((𝑂𝐴) ∪ (𝐴𝑥)) → (𝑂𝑦) = (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))))
5857eleq1d 2811 . . . . . . . . . . . . 13 (𝑦 = ((𝑂𝐴) ∪ (𝐴𝑥)) → ((𝑂𝑦) ∈ 𝑡 ↔ (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))) ∈ 𝑡))
5914simp2d 1140 . . . . . . . . . . . . . . 15 (𝑡𝐿 → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
6059ad2antlr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
61 difeq2 4115 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑂𝑥) = (𝑂𝑦))
6261eleq1d 2811 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂𝑦) ∈ 𝑡))
6362cbvralvw 3225 . . . . . . . . . . . . . 14 (∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ↔ ∀𝑦𝑡 (𝑂𝑦) ∈ 𝑡)
6460, 63sylib 217 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑦𝑡 (𝑂𝑦) ∈ 𝑡)
65 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑡𝐿)
6645, 23eleqtrdi 2836 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 {𝑡𝐿𝑇𝑡})
67 elintrabg 4969 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐸 → (𝐴 {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡𝐴𝑡)))
6845, 67syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡𝐴𝑡)))
6966, 68mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑡𝐿 (𝑇𝑡𝐴𝑡))
7069r19.21bi 3239 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝐿) → (𝑇𝑡𝐴𝑡))
7170imp 405 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑡)
7271adantllr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝐴𝑡)
73 difeq2 4115 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐴 → (𝑂𝑥) = (𝑂𝐴))
7473eleq1d 2811 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂𝐴) ∈ 𝑡))
7559adantr 479 . . . . . . . . . . . . . . . 16 ((𝑡𝐿𝐴𝑡) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
76 simpr 483 . . . . . . . . . . . . . . . 16 ((𝑡𝐿𝐴𝑡) → 𝐴𝑡)
7774, 75, 76rspcdva 3609 . . . . . . . . . . . . . . 15 ((𝑡𝐿𝐴𝑡) → (𝑂𝐴) ∈ 𝑡)
7865, 72, 77syl2anc 582 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑂𝐴) ∈ 𝑡)
79 simpllr 774 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸))
8079simprd 494 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝐸)
8180, 23eleqtrdi 2836 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡})
82 vex 3466 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
8382inex2 5323 . . . . . . . . . . . . . . . . 17 (𝐴𝑥) ∈ V
84 elintrabg 4969 . . . . . . . . . . . . . . . . 17 ((𝐴𝑥) ∈ V → ((𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡)))
8583, 84mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝐴𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡)))
8681, 85mpbid 231 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡))
87 simpr 483 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑇𝑡)
88 rspa 3236 . . . . . . . . . . . . . . . 16 ((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡))
8988imp 405 . . . . . . . . . . . . . . 15 (((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑥) ∈ 𝑡) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝑡)
9086, 65, 87, 89syl21anc 836 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑥) ∈ 𝑡)
91 incom 4202 . . . . . . . . . . . . . . . 16 ((𝑂𝐴) ∩ (𝐴𝑥)) = ((𝐴𝑥) ∩ (𝑂𝐴))
92 inss1 4230 . . . . . . . . . . . . . . . . 17 (𝐴𝑥) ⊆ 𝐴
93 disjdif 4476 . . . . . . . . . . . . . . . . 17 (𝐴 ∩ (𝑂𝐴)) = ∅
94 ssdisj 4464 . . . . . . . . . . . . . . . . 17 (((𝐴𝑥) ⊆ 𝐴 ∧ (𝐴 ∩ (𝑂𝐴)) = ∅) → ((𝐴𝑥) ∩ (𝑂𝐴)) = ∅)
9592, 93, 94mp2an 690 . . . . . . . . . . . . . . . 16 ((𝐴𝑥) ∩ (𝑂𝐴)) = ∅
9691, 95eqtri 2754 . . . . . . . . . . . . . . 15 ((𝑂𝐴) ∩ (𝐴𝑥)) = ∅
9796a1i 11 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝑂𝐴) ∩ (𝐴𝑥)) = ∅)
9812, 65, 78, 90, 97unelldsys 33991 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ((𝑂𝐴) ∪ (𝐴𝑥)) ∈ 𝑡)
9958, 64, 98rspcdva 3609 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑂 ∖ ((𝑂𝐴) ∪ (𝐴𝑥))) ∈ 𝑡)
10056, 99eqeltrd 2826 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)
101100ex 411 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡))
102101ralrimiva 3136 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡))
103 inex1g 5324 . . . . . . . . . . . 12 (𝐴𝐸 → (𝐴 ∩ (𝑂𝑥)) ∈ V)
10445, 103syl 17 . . . . . . . . . . 11 (𝜑 → (𝐴 ∩ (𝑂𝑥)) ∈ V)
105104adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ V)
106 elintrabg 4969 . . . . . . . . . 10 ((𝐴 ∩ (𝑂𝑥)) ∈ V → ((𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)))
107105, 106syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ((𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 ∩ (𝑂𝑥)) ∈ 𝑡)))
108102, 107mpbird 256 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ {𝑡𝐿𝑇𝑡})
109108, 23eleqtrrdi 2837 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸)
11032, 109jca 510 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ 𝒫 𝑂 ∧ (𝐴𝑥) ∈ 𝐸)) → ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
11128, 110sylan2b 592 . . . . 5 ((𝜑𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
112 ineq2 4207 . . . . . . 7 (𝑏 = (𝑂𝑥) → (𝐴𝑏) = (𝐴 ∩ (𝑂𝑥)))
113112eleq1d 2811 . . . . . 6 (𝑏 = (𝑂𝑥) → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
114113elrab 3681 . . . . 5 ((𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ ((𝑂𝑥) ∈ 𝒫 𝑂 ∧ (𝐴 ∩ (𝑂𝑥)) ∈ 𝐸))
115111, 114sylibr 233 . . . 4 ((𝜑𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
116115ralrimiva 3136 . . 3 (𝜑 → ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
117 ineq2 4207 . . . . . . 7 (𝑏 = 𝑥 → (𝐴𝑏) = (𝐴 𝑥))
118117eleq1d 2811 . . . . . 6 (𝑏 = 𝑥 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴 𝑥) ∈ 𝐸))
1191sspwi 4619 . . . . . . . 8 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ⊆ 𝒫 𝒫 𝑂
120 simplr 767 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
121119, 120sselid 3977 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝒫 𝑂)
122121elpwunicl 32475 . . . . . 6 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑂)
123 uniin2 32473 . . . . . . . . . . . 12 𝑦𝑥 (𝐴𝑦) = (𝐴 𝑥)
124 vex 3466 . . . . . . . . . . . . . 14 𝑦 ∈ V
125124inex2 5323 . . . . . . . . . . . . 13 (𝐴𝑦) ∈ V
126125dfiun3 5973 . . . . . . . . . . . 12 𝑦𝑥 (𝐴𝑦) = ran (𝑦𝑥 ↦ (𝐴𝑦))
127123, 126eqtr3i 2756 . . . . . . . . . . 11 (𝐴 𝑥) = ran (𝑦𝑥 ↦ (𝐴𝑦))
128 simplr 767 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑡𝐿)
129 nfv 1910 . . . . . . . . . . . . . . . . . 18 𝑦(𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
130 nfv 1910 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑥 ≼ ω
131 nfdisj1 5132 . . . . . . . . . . . . . . . . . . 19 𝑦Disj 𝑦𝑥 𝑦
132130, 131nfan 1895 . . . . . . . . . . . . . . . . . 18 𝑦(𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
133129, 132nfan 1895 . . . . . . . . . . . . . . . . 17 𝑦((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
134 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑦 𝑡𝐿
135133, 134nfan 1895 . . . . . . . . . . . . . . . 16 𝑦(((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿)
136 nfv 1910 . . . . . . . . . . . . . . . 16 𝑦 𝑇𝑡
137135, 136nfan 1895 . . . . . . . . . . . . . . 15 𝑦((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡)
138 elpwi 4614 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
139138ad4antlr 731 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑥 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
140139sselda 3979 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
141 ineq2 4207 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑦 → (𝐴𝑏) = (𝐴𝑦))
142141eleq1d 2811 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑦 → ((𝐴𝑏) ∈ 𝐸 ↔ (𝐴𝑦) ∈ 𝐸))
143142elrab 3681 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ↔ (𝑦 ∈ 𝒫 𝑂 ∧ (𝐴𝑦) ∈ 𝐸))
144143simprbi 495 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} → (𝐴𝑦) ∈ 𝐸)
145140, 144syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → (𝐴𝑦) ∈ 𝐸)
146 simpllr 774 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑡𝐿)
147 simplr 767 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → 𝑇𝑡)
14823eleq2i 2818 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑦) ∈ 𝐸 ↔ (𝐴𝑦) ∈ {𝑡𝐿𝑇𝑡})
149125elintrab 4968 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑦) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
150148, 149bitri 274 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑦) ∈ 𝐸 ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
151 rspa 3236 . . . . . . . . . . . . . . . . . . 19 ((∀𝑡𝐿 (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
152150, 151sylanb 579 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ∈ 𝐸𝑡𝐿) → (𝑇𝑡 → (𝐴𝑦) ∈ 𝑡))
153152imp 405 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑦) ∈ 𝐸𝑡𝐿) ∧ 𝑇𝑡) → (𝐴𝑦) ∈ 𝑡)
154145, 146, 147, 153syl21anc 836 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) ∧ 𝑦𝑥) → (𝐴𝑦) ∈ 𝑡)
155154ex 411 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑦𝑥 → (𝐴𝑦) ∈ 𝑡))
156137, 155ralrimi 3245 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ∀𝑦𝑥 (𝐴𝑦) ∈ 𝑡)
157 eqid 2726 . . . . . . . . . . . . . . 15 (𝑦𝑥 ↦ (𝐴𝑦)) = (𝑦𝑥 ↦ (𝐴𝑦))
158157rnmptss 7137 . . . . . . . . . . . . . 14 (∀𝑦𝑥 (𝐴𝑦) ∈ 𝑡 → ran (𝑦𝑥 ↦ (𝐴𝑦)) ⊆ 𝑡)
159156, 158syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ⊆ 𝑡)
160128, 159sselpwd 5333 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡)
161 simpllr 774 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
162161simpld 493 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → 𝑥 ≼ ω)
163 1stcrestlem 23447 . . . . . . . . . . . . 13 (𝑥 ≼ ω → ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω)
164162, 163syl 17 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω)
165161simprd 494 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑦𝑥 𝑦)
166 disjin2 32507 . . . . . . . . . . . . . 14 (Disj 𝑦𝑥 𝑦Disj 𝑦𝑥 (𝐴𝑦))
167 disjrnmpt 32505 . . . . . . . . . . . . . 14 (Disj 𝑦𝑥 (𝐴𝑦) → Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
168165, 166, 1673syl 18 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
169 nfmpt1 5261 . . . . . . . . . . . . . . 15 𝑦(𝑦𝑥 ↦ (𝐴𝑦))
170169nfrn 5958 . . . . . . . . . . . . . 14 𝑦ran (𝑦𝑥 ↦ (𝐴𝑦))
171 nfcv 2892 . . . . . . . . . . . . . 14 𝑧𝑦
172 nfcv 2892 . . . . . . . . . . . . . 14 𝑦𝑧
173 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑧𝑦 = 𝑧)
174170, 171, 172, 173cbvdisjf 32491 . . . . . . . . . . . . 13 (Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦Disj 𝑧 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑧)
175168, 174sylibr 233 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)
176 breq1 5156 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (𝑧 ≼ ω ↔ ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω))
177172, 170disjeq1f 32493 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (Disj 𝑦𝑧 𝑦Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦))
178176, 177anbi12d 630 . . . . . . . . . . . . . . 15 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → ((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) ↔ (ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)))
179 unieq 4924 . . . . . . . . . . . . . . . 16 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → 𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)))
180179eleq1d 2811 . . . . . . . . . . . . . . 15 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → ( 𝑧𝑡 ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡))
181178, 180imbi12d 343 . . . . . . . . . . . . . 14 (𝑧 = ran (𝑦𝑥 ↦ (𝐴𝑦)) → (((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡) ↔ ((ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)))
18214simp3d 1141 . . . . . . . . . . . . . . . 16 (𝑡𝐿 → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
183 breq1 5156 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (𝑥 ≼ ω ↔ 𝑧 ≼ ω))
184 disjeq1 5125 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (Disj 𝑦𝑥 𝑦Disj 𝑦𝑧 𝑦))
185183, 184anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) ↔ (𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦)))
186 unieq 4924 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 𝑥 = 𝑧)
187186eleq1d 2811 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ( 𝑥𝑡 𝑧𝑡))
188185, 187imbi12d 343 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡)))
189188cbvralvw 3225 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
190182, 189sylib 217 . . . . . . . . . . . . . . 15 (𝑡𝐿 → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
191190adantr 479 . . . . . . . . . . . . . 14 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ∀𝑧 ∈ 𝒫 𝑡((𝑧 ≼ ω ∧ Disj 𝑦𝑧 𝑦) → 𝑧𝑡))
192 simpr 483 . . . . . . . . . . . . . 14 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡)
193181, 191, 192rspcdva 3609 . . . . . . . . . . . . 13 ((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) → ((ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡))
194193imp 405 . . . . . . . . . . . 12 (((𝑡𝐿 ∧ ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝒫 𝑡) ∧ (ran (𝑦𝑥 ↦ (𝐴𝑦)) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑦𝑥 ↦ (𝐴𝑦))𝑦)) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)
195128, 160, 164, 175, 194syl22anc 837 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → ran (𝑦𝑥 ↦ (𝐴𝑦)) ∈ 𝑡)
196127, 195eqeltrid 2830 . . . . . . . . . 10 (((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝑇𝑡) → (𝐴 𝑥) ∈ 𝑡)
197196ex 411 . . . . . . . . 9 ((((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) → (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
198197ralrimiva 3136 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → ∀𝑡𝐿 (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
199 vuniex 7750 . . . . . . . . . 10 𝑥 ∈ V
200199inex2 5323 . . . . . . . . 9 (𝐴 𝑥) ∈ V
201200elintrab 4968 . . . . . . . 8 ((𝐴 𝑥) ∈ {𝑡𝐿𝑇𝑡} ↔ ∀𝑡𝐿 (𝑇𝑡 → (𝐴 𝑥) ∈ 𝑡))
202198, 201sylibr 233 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝐴 𝑥) ∈ {𝑡𝐿𝑇𝑡})
203202, 23eleqtrrdi 2837 . . . . . 6 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝐴 𝑥) ∈ 𝐸)
204118, 122, 203elrabd 3683 . . . . 5 (((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})
205204ex 411 . . . 4 ((𝜑𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))
206205ralrimiva 3136 . . 3 (𝜑 → ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))
20725, 116, 2063jca 1125 . 2 (𝜑 → (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸})))
20812isldsys 33989 . 2 ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝐿 ↔ ({𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} (𝑂𝑥) ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∧ ∀𝑥 ∈ 𝒫 {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 ∈ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸}))))
2097, 207, 208sylanbrc 581 1 (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴𝑏) ∈ 𝐸} ∈ 𝐿)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wral 3051  {crab 3419  Vcvv 3462  cdif 3944  cun 3945  cin 3946  wss 3947  c0 4325  𝒫 cpw 4607   cuni 4913   cint 4954   ciun 5001  Disj wdisj 5118   class class class wbr 5153  cmpt 5236  ran crn 5683  cfv 6554  ωcom 7876  cdom 8972  ficfi 9453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-disj 5119  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-er 8734  df-map 8857  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-oi 9553  df-dju 9944  df-card 9982  df-acn 9985
This theorem is referenced by:  ldgenpisyslem2  33997
  Copyright terms: Public domain W3C validator