Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clcnvlem Structured version   Visualization version   GIF version

Theorem clcnvlem 37438
Description: When 𝐴, an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
Hypotheses
Ref Expression
clcnvlem.sub1 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → (𝜒𝜓))
clcnvlem.sub2 ((𝜑𝑦 = 𝑥) → (𝜓𝜒))
clcnvlem.sub3 (𝑥 = 𝐴 → (𝜓𝜃))
clcnvlem.ssub (𝜑𝑋𝐴)
clcnvlem.ubex (𝜑𝐴 ∈ V)
clcnvlem.clex (𝜑𝜃)
Assertion
Ref Expression
clcnvlem (𝜑 {𝑥 ∣ (𝑋𝑥𝜓)} = {𝑦 ∣ (𝑋𝑦𝜒)})
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝑋   𝜑,𝑥,𝑦   𝜓,𝑦   𝜒,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦)   𝜃(𝑦)   𝐴(𝑦)

Proof of Theorem clcnvlem
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 clcnvlem.ubex . . . 4 (𝜑𝐴 ∈ V)
2 clcnvlem.ssub . . . . 5 (𝜑𝑋𝐴)
3 clcnvlem.clex . . . . 5 (𝜑𝜃)
42, 3jca 554 . . . 4 (𝜑 → (𝑋𝐴𝜃))
5 clcnvlem.sub3 . . . . 5 (𝑥 = 𝐴 → (𝜓𝜃))
65cleq2lem 37422 . . . 4 (𝑥 = 𝐴 → ((𝑋𝑥𝜓) ↔ (𝑋𝐴𝜃)))
71, 4, 6elabd 3339 . . 3 (𝜑 → ∃𝑥(𝑋𝑥𝜓))
87cnvintabd 37417 . 2 (𝜑 {𝑥 ∣ (𝑋𝑥𝜓)} = {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
9 df-rab 2916 . . . . 5 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))}
10 exsimpl 1792 . . . . . . . . . . 11 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → ∃𝑥 𝑧 = 𝑥)
11 relcnv 5467 . . . . . . . . . . . . 13 Rel 𝑥
12 releq 5167 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (Rel 𝑧 ↔ Rel 𝑥))
1311, 12mpbiri 248 . . . . . . . . . . . 12 (𝑧 = 𝑥 → Rel 𝑧)
1413exlimiv 1855 . . . . . . . . . . 11 (∃𝑥 𝑧 = 𝑥 → Rel 𝑧)
1510, 14syl 17 . . . . . . . . . 10 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → Rel 𝑧)
16 df-rel 5086 . . . . . . . . . 10 (Rel 𝑧𝑧 ⊆ (V × V))
1715, 16sylib 208 . . . . . . . . 9 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → 𝑧 ⊆ (V × V))
18 selpw 4142 . . . . . . . . . 10 (𝑧 ∈ 𝒫 (V × V) ↔ 𝑧 ⊆ (V × V))
1918bicomi 214 . . . . . . . . 9 (𝑧 ⊆ (V × V) ↔ 𝑧 ∈ 𝒫 (V × V))
2017, 19sylib 208 . . . . . . . 8 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → 𝑧 ∈ 𝒫 (V × V))
2120pm4.71ri 664 . . . . . . 7 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))))
2221bicomi 214 . . . . . 6 ((𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))) ↔ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))
2322abbii 2736 . . . . 5 {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
249, 23eqtri 2643 . . . 4 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
2524inteqi 4449 . . 3 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
2625a1i 11 . 2 (𝜑 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
27 vex 3192 . . . . . . 7 𝑦 ∈ V
2827cnvex 7067 . . . . . 6 𝑦 ∈ V
2928cnvex 7067 . . . . 5 𝑦 ∈ V
3029a1i 11 . . . 4 (𝜑𝑦 ∈ V)
311, 2ssexd 4770 . . . . . . . . . . 11 (𝜑𝑋 ∈ V)
32 difexg 4773 . . . . . . . . . . 11 (𝑋 ∈ V → (𝑋𝑋) ∈ V)
3331, 32syl 17 . . . . . . . . . 10 (𝜑 → (𝑋𝑋) ∈ V)
34 unexg 6919 . . . . . . . . . 10 ((𝑦 ∈ V ∧ (𝑋𝑋) ∈ V) → (𝑦 ∪ (𝑋𝑋)) ∈ V)
3528, 33, 34sylancr 694 . . . . . . . . 9 (𝜑 → (𝑦 ∪ (𝑋𝑋)) ∈ V)
36 inundif 4023 . . . . . . . . . . . . . 14 ((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋
37 cnvun 5502 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝑋) ∪ (𝑋𝑋)) = ((𝑋𝑋) ∪ (𝑋𝑋))
3837sseq1i 3613 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 ↔ ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦)
3938biimpi 206 . . . . . . . . . . . . . . . . . . 19 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦)
4039unssad 3773 . . . . . . . . . . . . . . . . . 18 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦(𝑋𝑋) ⊆ 𝑦)
41 relcnv 5467 . . . . . . . . . . . . . . . . . . . . 21 Rel 𝑋
42 relin2 5203 . . . . . . . . . . . . . . . . . . . . 21 (Rel 𝑋 → Rel (𝑋𝑋))
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Rel (𝑋𝑋)
44 dfrel2 5547 . . . . . . . . . . . . . . . . . . . 20 (Rel (𝑋𝑋) ↔ (𝑋𝑋) = (𝑋𝑋))
4543, 44mpbi 220 . . . . . . . . . . . . . . . . . . 19 (𝑋𝑋) = (𝑋𝑋)
46 cnvss 5259 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝑋) ⊆ 𝑦(𝑋𝑋) ⊆ 𝑦)
4745, 46syl5eqssr 3634 . . . . . . . . . . . . . . . . . 18 ((𝑋𝑋) ⊆ 𝑦 → (𝑋𝑋) ⊆ 𝑦)
4840, 47syl 17 . . . . . . . . . . . . . . . . 17 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → (𝑋𝑋) ⊆ 𝑦)
49 ssid 3608 . . . . . . . . . . . . . . . . 17 (𝑋𝑋) ⊆ (𝑋𝑋)
50 unss12 3768 . . . . . . . . . . . . . . . . 17 (((𝑋𝑋) ⊆ 𝑦 ∧ (𝑋𝑋) ⊆ (𝑋𝑋)) → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)))
5148, 49, 50sylancl 693 . . . . . . . . . . . . . . . 16 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)))
5251a1i 11 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋))))
53 cnveq 5261 . . . . . . . . . . . . . . . 16 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋)
5453sseq1d 3616 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦𝑋𝑦))
55 sseq1 3610 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)) ↔ 𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5652, 54, 553imtr3d 282 . . . . . . . . . . . . . 14 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (𝑋𝑦𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5736, 56ax-mp 5 . . . . . . . . . . . . 13 (𝑋𝑦𝑋 ⊆ (𝑦 ∪ (𝑋𝑋)))
58 sseq2 3611 . . . . . . . . . . . . 13 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑋𝑥𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5957, 58syl5ibr 236 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑋𝑦𝑋𝑥))
6059adantl 482 . . . . . . . . . . 11 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → (𝑋𝑦𝑋𝑥))
61 clcnvlem.sub1 . . . . . . . . . . 11 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → (𝜒𝜓))
6260, 61anim12d 585 . . . . . . . . . 10 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑋𝑦𝜒) → (𝑋𝑥𝜓)))
63 cnveq 5261 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑥 = (𝑦 ∪ (𝑋𝑋)))
64 cnvun 5502 . . . . . . . . . . . . 13 (𝑦 ∪ (𝑋𝑋)) = (𝑦(𝑋𝑋))
65 cnvnonrel 37402 . . . . . . . . . . . . . . 15 (𝑋𝑋) = ∅
66 0ss 3949 . . . . . . . . . . . . . . 15 ∅ ⊆ 𝑦
6765, 66eqsstri 3619 . . . . . . . . . . . . . 14 (𝑋𝑋) ⊆ 𝑦
68 ssequn2 3769 . . . . . . . . . . . . . 14 ((𝑋𝑋) ⊆ 𝑦 ↔ (𝑦(𝑋𝑋)) = 𝑦)
6967, 68mpbi 220 . . . . . . . . . . . . 13 (𝑦(𝑋𝑋)) = 𝑦
7064, 69eqtr2i 2644 . . . . . . . . . . . 12 𝑦 = (𝑦 ∪ (𝑋𝑋))
7163, 70syl6reqr 2674 . . . . . . . . . . 11 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑦 = 𝑥)
7271adantl 482 . . . . . . . . . 10 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → 𝑦 = 𝑥)
7362, 72jctild 565 . . . . . . . . 9 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑋𝑦𝜒) → (𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7435, 73spcimedv 3281 . . . . . . . 8 (𝜑 → ((𝑋𝑦𝜒) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7574imp 445 . . . . . . 7 ((𝜑 ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓)))
7675adantlr 750 . . . . . 6 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓)))
77 eqeq1 2625 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
7877anbi1d 740 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ (𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7978exbidv 1847 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
8079ad2antlr 762 . . . . . 6 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
8176, 80mpbird 247 . . . . 5 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))
8281ex 450 . . . 4 ((𝜑𝑧 = 𝑦) → ((𝑋𝑦𝜒) → ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))))
83 cnvcnvss 5553 . . . . 5 𝑦𝑦
8483a1i 11 . . . 4 (𝜑𝑦𝑦)
8530, 82, 84intabssd 37424 . . 3 (𝜑 {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} ⊆ {𝑦 ∣ (𝑋𝑦𝜒)})
86 vex 3192 . . . . 5 𝑧 ∈ V
8786a1i 11 . . . 4 (𝜑𝑧 ∈ V)
88 eqtr 2640 . . . . . . . 8 ((𝑦 = 𝑧𝑧 = 𝑥) → 𝑦 = 𝑥)
89 cnvss 5259 . . . . . . . . . . . 12 (𝑋𝑥𝑋𝑥)
90 sseq2 3611 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑋𝑦𝑋𝑥))
9189, 90syl5ibr 236 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝑋𝑥𝑋𝑦))
9291adantl 482 . . . . . . . . . 10 ((𝜑𝑦 = 𝑥) → (𝑋𝑥𝑋𝑦))
93 clcnvlem.sub2 . . . . . . . . . 10 ((𝜑𝑦 = 𝑥) → (𝜓𝜒))
9492, 93anim12d 585 . . . . . . . . 9 ((𝜑𝑦 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒)))
9594ex 450 . . . . . . . 8 (𝜑 → (𝑦 = 𝑥 → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒))))
9688, 95syl5 34 . . . . . . 7 (𝜑 → ((𝑦 = 𝑧𝑧 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒))))
9796impl 649 . . . . . 6 (((𝜑𝑦 = 𝑧) ∧ 𝑧 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒)))
9897expimpd 628 . . . . 5 ((𝜑𝑦 = 𝑧) → ((𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → (𝑋𝑦𝜒)))
9998exlimdv 1858 . . . 4 ((𝜑𝑦 = 𝑧) → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → (𝑋𝑦𝜒)))
100 ssid 3608 . . . . 5 𝑧𝑧
101100a1i 11 . . . 4 (𝜑𝑧𝑧)
10287, 99, 101intabssd 37424 . . 3 (𝜑 {𝑦 ∣ (𝑋𝑦𝜒)} ⊆ {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
10385, 102eqssd 3604 . 2 (𝜑 {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑦 ∣ (𝑋𝑦𝜒)})
1048, 26, 1033eqtrd 2659 1 (𝜑 {𝑥 ∣ (𝑋𝑥𝜓)} = {𝑦 ∣ (𝑋𝑦𝜒)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  {cab 2607  {crab 2911  Vcvv 3189  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135   cint 4445   × cxp 5077  ccnv 5078  Rel wrel 5084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-int 4446  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-iota 5815  df-fun 5854  df-fv 5860  df-1st 7120  df-2nd 7121
This theorem is referenced by:  cnvtrucl0  37439  cnvrcl0  37440  cnvtrcl0  37441
  Copyright terms: Public domain W3C validator