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 38456
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 501 . . . 4 (𝜑 → (𝑋𝐴𝜃))
5 clcnvlem.sub3 . . . . 5 (𝑥 = 𝐴 → (𝜓𝜃))
65cleq2lem 38440 . . . 4 (𝑥 = 𝐴 → ((𝑋𝑥𝜓) ↔ (𝑋𝐴𝜃)))
71, 4, 6elabd 3503 . . 3 (𝜑 → ∃𝑥(𝑋𝑥𝜓))
87cnvintabd 38435 . 2 (𝜑 {𝑥 ∣ (𝑋𝑥𝜓)} = {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
9 df-rab 3070 . . . . 5 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))}
10 exsimpl 1946 . . . . . . . . . . 11 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → ∃𝑥 𝑧 = 𝑥)
11 relcnv 5643 . . . . . . . . . . . . 13 Rel 𝑥
12 releq 5340 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (Rel 𝑧 ↔ Rel 𝑥))
1311, 12mpbiri 248 . . . . . . . . . . . 12 (𝑧 = 𝑥 → Rel 𝑧)
1413exlimiv 2010 . . . . . . . . . . 11 (∃𝑥 𝑧 = 𝑥 → Rel 𝑧)
1510, 14syl 17 . . . . . . . . . 10 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → Rel 𝑧)
16 df-rel 5257 . . . . . . . . . 10 (Rel 𝑧𝑧 ⊆ (V × V))
1715, 16sylib 208 . . . . . . . . 9 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → 𝑧 ⊆ (V × V))
18 selpw 4305 . . . . . . . . . 10 (𝑧 ∈ 𝒫 (V × V) ↔ 𝑧 ⊆ (V × V))
1918bicomi 214 . . . . . . . . 9 (𝑧 ⊆ (V × V) ↔ 𝑧 ∈ 𝒫 (V × V))
2017, 19sylib 208 . . . . . . . 8 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → 𝑧 ∈ 𝒫 (V × V))
2120pm4.71ri 550 . . . . . . 7 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))))
2221bicomi 214 . . . . . 6 ((𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))) ↔ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))
2322abbii 2888 . . . . 5 {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
249, 23eqtri 2793 . . . 4 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
2524inteqi 4616 . . 3 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
2625a1i 11 . 2 (𝜑 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
27 vex 3354 . . . . . . 7 𝑦 ∈ V
2827cnvex 7263 . . . . . 6 𝑦 ∈ V
2928cnvex 7263 . . . . 5 𝑦 ∈ V
3029a1i 11 . . . 4 (𝜑𝑦 ∈ V)
311, 2ssexd 4940 . . . . . . . . . . 11 (𝜑𝑋 ∈ V)
32 difexg 4943 . . . . . . . . . . 11 (𝑋 ∈ V → (𝑋𝑋) ∈ V)
3331, 32syl 17 . . . . . . . . . 10 (𝜑 → (𝑋𝑋) ∈ V)
34 unexg 7109 . . . . . . . . . 10 ((𝑦 ∈ V ∧ (𝑋𝑋) ∈ V) → (𝑦 ∪ (𝑋𝑋)) ∈ V)
3528, 33, 34sylancr 575 . . . . . . . . 9 (𝜑 → (𝑦 ∪ (𝑋𝑋)) ∈ V)
36 inundif 4189 . . . . . . . . . . . . . 14 ((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋
37 cnvun 5678 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝑋) ∪ (𝑋𝑋)) = ((𝑋𝑋) ∪ (𝑋𝑋))
3837sseq1i 3778 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 ↔ ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦)
3938biimpi 206 . . . . . . . . . . . . . . . . . . 19 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦)
4039unssad 3941 . . . . . . . . . . . . . . . . . 18 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦(𝑋𝑋) ⊆ 𝑦)
41 relcnv 5643 . . . . . . . . . . . . . . . . . . . . 21 Rel 𝑋
42 relin2 5375 . . . . . . . . . . . . . . . . . . . . 21 (Rel 𝑋 → Rel (𝑋𝑋))
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Rel (𝑋𝑋)
44 dfrel2 5723 . . . . . . . . . . . . . . . . . . . 20 (Rel (𝑋𝑋) ↔ (𝑋𝑋) = (𝑋𝑋))
4543, 44mpbi 220 . . . . . . . . . . . . . . . . . . 19 (𝑋𝑋) = (𝑋𝑋)
46 cnvss 5432 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝑋) ⊆ 𝑦(𝑋𝑋) ⊆ 𝑦)
4745, 46syl5eqssr 3799 . . . . . . . . . . . . . . . . . 18 ((𝑋𝑋) ⊆ 𝑦 → (𝑋𝑋) ⊆ 𝑦)
4840, 47syl 17 . . . . . . . . . . . . . . . . 17 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → (𝑋𝑋) ⊆ 𝑦)
49 ssid 3773 . . . . . . . . . . . . . . . . 17 (𝑋𝑋) ⊆ (𝑋𝑋)
50 unss12 3936 . . . . . . . . . . . . . . . . 17 (((𝑋𝑋) ⊆ 𝑦 ∧ (𝑋𝑋) ⊆ (𝑋𝑋)) → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)))
5148, 49, 50sylancl 574 . . . . . . . . . . . . . . . 16 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)))
5251a1i 11 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋))))
53 cnveq 5433 . . . . . . . . . . . . . . . 16 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋)
5453sseq1d 3781 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦𝑋𝑦))
55 sseq1 3775 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)) ↔ 𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5652, 54, 553imtr3d 282 . . . . . . . . . . . . . 14 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (𝑋𝑦𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5736, 56ax-mp 5 . . . . . . . . . . . . 13 (𝑋𝑦𝑋 ⊆ (𝑦 ∪ (𝑋𝑋)))
58 sseq2 3776 . . . . . . . . . . . . 13 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑋𝑥𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5957, 58syl5ibr 236 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑋𝑦𝑋𝑥))
6059adantl 467 . . . . . . . . . . 11 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → (𝑋𝑦𝑋𝑥))
61 clcnvlem.sub1 . . . . . . . . . . 11 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → (𝜒𝜓))
6260, 61anim12d 596 . . . . . . . . . 10 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑋𝑦𝜒) → (𝑋𝑥𝜓)))
63 cnveq 5433 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑥 = (𝑦 ∪ (𝑋𝑋)))
64 cnvun 5678 . . . . . . . . . . . . 13 (𝑦 ∪ (𝑋𝑋)) = (𝑦(𝑋𝑋))
65 cnvnonrel 38420 . . . . . . . . . . . . . . 15 (𝑋𝑋) = ∅
66 0ss 4117 . . . . . . . . . . . . . . 15 ∅ ⊆ 𝑦
6765, 66eqsstri 3784 . . . . . . . . . . . . . 14 (𝑋𝑋) ⊆ 𝑦
68 ssequn2 3937 . . . . . . . . . . . . . 14 ((𝑋𝑋) ⊆ 𝑦 ↔ (𝑦(𝑋𝑋)) = 𝑦)
6967, 68mpbi 220 . . . . . . . . . . . . 13 (𝑦(𝑋𝑋)) = 𝑦
7064, 69eqtr2i 2794 . . . . . . . . . . . 12 𝑦 = (𝑦 ∪ (𝑋𝑋))
7163, 70syl6reqr 2824 . . . . . . . . . . 11 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑦 = 𝑥)
7271adantl 467 . . . . . . . . . 10 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → 𝑦 = 𝑥)
7362, 72jctild 515 . . . . . . . . 9 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑋𝑦𝜒) → (𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7435, 73spcimedv 3443 . . . . . . . 8 (𝜑 → ((𝑋𝑦𝜒) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7574imp 393 . . . . . . 7 ((𝜑 ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓)))
7675adantlr 694 . . . . . 6 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓)))
77 eqeq1 2775 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
7877anbi1d 615 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ (𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7978exbidv 2002 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
8079ad2antlr 706 . . . . . 6 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
8176, 80mpbird 247 . . . . 5 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))
8281ex 397 . . . 4 ((𝜑𝑧 = 𝑦) → ((𝑋𝑦𝜒) → ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))))
83 cnvcnvss 5729 . . . . 5 𝑦𝑦
8483a1i 11 . . . 4 (𝜑𝑦𝑦)
8530, 82, 84intabssd 38442 . . 3 (𝜑 {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} ⊆ {𝑦 ∣ (𝑋𝑦𝜒)})
86 vex 3354 . . . . 5 𝑧 ∈ V
8786a1i 11 . . . 4 (𝜑𝑧 ∈ V)
88 eqtr 2790 . . . . . . . 8 ((𝑦 = 𝑧𝑧 = 𝑥) → 𝑦 = 𝑥)
89 cnvss 5432 . . . . . . . . . . . 12 (𝑋𝑥𝑋𝑥)
90 sseq2 3776 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑋𝑦𝑋𝑥))
9189, 90syl5ibr 236 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝑋𝑥𝑋𝑦))
9291adantl 467 . . . . . . . . . 10 ((𝜑𝑦 = 𝑥) → (𝑋𝑥𝑋𝑦))
93 clcnvlem.sub2 . . . . . . . . . 10 ((𝜑𝑦 = 𝑥) → (𝜓𝜒))
9492, 93anim12d 596 . . . . . . . . 9 ((𝜑𝑦 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒)))
9594ex 397 . . . . . . . 8 (𝜑 → (𝑦 = 𝑥 → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒))))
9688, 95syl5 34 . . . . . . 7 (𝜑 → ((𝑦 = 𝑧𝑧 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒))))
9796impl 443 . . . . . 6 (((𝜑𝑦 = 𝑧) ∧ 𝑧 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒)))
9897expimpd 441 . . . . 5 ((𝜑𝑦 = 𝑧) → ((𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → (𝑋𝑦𝜒)))
9998exlimdv 2013 . . . 4 ((𝜑𝑦 = 𝑧) → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → (𝑋𝑦𝜒)))
100 ssid 3773 . . . . 5 𝑧𝑧
101100a1i 11 . . . 4 (𝜑𝑧𝑧)
10287, 99, 101intabssd 38442 . . 3 (𝜑 {𝑦 ∣ (𝑋𝑦𝜒)} ⊆ {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
10385, 102eqssd 3769 . 2 (𝜑 {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑦 ∣ (𝑋𝑦𝜒)})
1048, 26, 1033eqtrd 2809 1 (𝜑 {𝑥 ∣ (𝑋𝑥𝜓)} = {𝑦 ∣ (𝑋𝑦𝜒)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  {cab 2757  {crab 3065  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  𝒫 cpw 4298   cint 4612   × cxp 5248  ccnv 5249  Rel wrel 5255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-int 4613  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-iota 5993  df-fun 6032  df-fv 6038  df-1st 7318  df-2nd 7319
This theorem is referenced by:  cnvtrucl0  38457  cnvrcl0  38458  cnvtrcl0  38459
  Copyright terms: Public domain W3C validator