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 38449
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 495 . . . 4 (𝜑 → (𝑋𝐴𝜃))
5 clcnvlem.sub3 . . . . 5 (𝑥 = 𝐴 → (𝜓𝜃))
65cleq2lem 38433 . . . 4 (𝑥 = 𝐴 → ((𝑋𝑥𝜓) ↔ (𝑋𝐴𝜃)))
71, 4, 6elabd 3501 . . 3 (𝜑 → ∃𝑥(𝑋𝑥𝜓))
87cnvintabd 38428 . 2 (𝜑 {𝑥 ∣ (𝑋𝑥𝜓)} = {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
9 df-rab 3069 . . . . 5 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))}
10 exsimpl 1945 . . . . . . . . . . 11 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → ∃𝑥 𝑧 = 𝑥)
11 relcnv 5644 . . . . . . . . . . . . 13 Rel 𝑥
12 releq 5341 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (Rel 𝑧 ↔ Rel 𝑥))
1311, 12mpbiri 248 . . . . . . . . . . . 12 (𝑧 = 𝑥 → Rel 𝑧)
1413exlimiv 2009 . . . . . . . . . . 11 (∃𝑥 𝑧 = 𝑥 → Rel 𝑧)
1510, 14syl 17 . . . . . . . . . 10 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → Rel 𝑧)
16 df-rel 5256 . . . . . . . . . 10 (Rel 𝑧𝑧 ⊆ (V × V))
1715, 16sylib 208 . . . . . . . . 9 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → 𝑧 ⊆ (V × V))
18 selpw 4302 . . . . . . . . . 10 (𝑧 ∈ 𝒫 (V × V) ↔ 𝑧 ⊆ (V × V))
1918bicomi 214 . . . . . . . . 9 (𝑧 ⊆ (V × V) ↔ 𝑧 ∈ 𝒫 (V × V))
2017, 19sylib 208 . . . . . . . 8 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → 𝑧 ∈ 𝒫 (V × V))
2120pm4.71ri 542 . . . . . . 7 (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))))
2221bicomi 214 . . . . . 6 ((𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))) ↔ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))
2322abbii 2887 . . . . 5 {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
249, 23eqtri 2792 . . . 4 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
2524inteqi 4613 . . 3 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))}
2625a1i 11 . 2 (𝜑 {𝑧 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
27 vex 3352 . . . . . . 7 𝑦 ∈ V
2827cnvex 7259 . . . . . 6 𝑦 ∈ V
2928cnvex 7259 . . . . 5 𝑦 ∈ V
3029a1i 11 . . . 4 (𝜑𝑦 ∈ V)
311, 2ssexd 4936 . . . . . . . . . . 11 (𝜑𝑋 ∈ V)
32 difexg 4939 . . . . . . . . . . 11 (𝑋 ∈ V → (𝑋𝑋) ∈ V)
3331, 32syl 17 . . . . . . . . . 10 (𝜑 → (𝑋𝑋) ∈ V)
34 unexg 7105 . . . . . . . . . 10 ((𝑦 ∈ V ∧ (𝑋𝑋) ∈ V) → (𝑦 ∪ (𝑋𝑋)) ∈ V)
3528, 33, 34sylancr 567 . . . . . . . . 9 (𝜑 → (𝑦 ∪ (𝑋𝑋)) ∈ V)
36 inundif 4186 . . . . . . . . . . . . . 14 ((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋
37 cnvun 5679 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋𝑋) ∪ (𝑋𝑋)) = ((𝑋𝑋) ∪ (𝑋𝑋))
3837sseq1i 3776 . . . . . . . . . . . . . . . . . . . 20 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 ↔ ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦)
3938biimpi 206 . . . . . . . . . . . . . . . . . . 19 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦)
4039unssad 3939 . . . . . . . . . . . . . . . . . 18 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦(𝑋𝑋) ⊆ 𝑦)
41 relcnv 5644 . . . . . . . . . . . . . . . . . . . . 21 Rel 𝑋
42 relin2 5376 . . . . . . . . . . . . . . . . . . . . 21 (Rel 𝑋 → Rel (𝑋𝑋))
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 Rel (𝑋𝑋)
44 dfrel2 5724 . . . . . . . . . . . . . . . . . . . 20 (Rel (𝑋𝑋) ↔ (𝑋𝑋) = (𝑋𝑋))
4543, 44mpbi 220 . . . . . . . . . . . . . . . . . . 19 (𝑋𝑋) = (𝑋𝑋)
46 cnvss 5433 . . . . . . . . . . . . . . . . . . 19 ((𝑋𝑋) ⊆ 𝑦(𝑋𝑋) ⊆ 𝑦)
4745, 46syl5eqssr 3797 . . . . . . . . . . . . . . . . . 18 ((𝑋𝑋) ⊆ 𝑦 → (𝑋𝑋) ⊆ 𝑦)
4840, 47syl 17 . . . . . . . . . . . . . . . . 17 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → (𝑋𝑋) ⊆ 𝑦)
49 ssid 3771 . . . . . . . . . . . . . . . . 17 (𝑋𝑋) ⊆ (𝑋𝑋)
50 unss12 3934 . . . . . . . . . . . . . . . . 17 (((𝑋𝑋) ⊆ 𝑦 ∧ (𝑋𝑋) ⊆ (𝑋𝑋)) → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)))
5148, 49, 50sylancl 566 . . . . . . . . . . . . . . . 16 (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)))
5251a1i 11 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦 → ((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋))))
53 cnveq 5434 . . . . . . . . . . . . . . . 16 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋)
5453sseq1d 3779 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ 𝑦𝑋𝑦))
55 sseq1 3773 . . . . . . . . . . . . . . 15 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (((𝑋𝑋) ∪ (𝑋𝑋)) ⊆ (𝑦 ∪ (𝑋𝑋)) ↔ 𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5652, 54, 553imtr3d 282 . . . . . . . . . . . . . 14 (((𝑋𝑋) ∪ (𝑋𝑋)) = 𝑋 → (𝑋𝑦𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5736, 56ax-mp 5 . . . . . . . . . . . . 13 (𝑋𝑦𝑋 ⊆ (𝑦 ∪ (𝑋𝑋)))
58 sseq2 3774 . . . . . . . . . . . . 13 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑋𝑥𝑋 ⊆ (𝑦 ∪ (𝑋𝑋))))
5957, 58syl5ibr 236 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑋𝑦𝑋𝑥))
6059adantl 467 . . . . . . . . . . 11 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → (𝑋𝑦𝑋𝑥))
61 clcnvlem.sub1 . . . . . . . . . . 11 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → (𝜒𝜓))
6260, 61anim12d 588 . . . . . . . . . 10 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑋𝑦𝜒) → (𝑋𝑥𝜓)))
63 cnveq 5434 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑥 = (𝑦 ∪ (𝑋𝑋)))
64 cnvun 5679 . . . . . . . . . . . . 13 (𝑦 ∪ (𝑋𝑋)) = (𝑦(𝑋𝑋))
65 cnvnonrel 38413 . . . . . . . . . . . . . . 15 (𝑋𝑋) = ∅
66 0ss 4114 . . . . . . . . . . . . . . 15 ∅ ⊆ 𝑦
6765, 66eqsstri 3782 . . . . . . . . . . . . . 14 (𝑋𝑋) ⊆ 𝑦
68 ssequn2 3935 . . . . . . . . . . . . . 14 ((𝑋𝑋) ⊆ 𝑦 ↔ (𝑦(𝑋𝑋)) = 𝑦)
6967, 68mpbi 220 . . . . . . . . . . . . 13 (𝑦(𝑋𝑋)) = 𝑦
7064, 69eqtr2i 2793 . . . . . . . . . . . 12 𝑦 = (𝑦 ∪ (𝑋𝑋))
7163, 70syl6reqr 2823 . . . . . . . . . . 11 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑦 = 𝑥)
7271adantl 467 . . . . . . . . . 10 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → 𝑦 = 𝑥)
7362, 72jctild 509 . . . . . . . . 9 ((𝜑𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑋𝑦𝜒) → (𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7435, 73spcimedv 3441 . . . . . . . 8 (𝜑 → ((𝑋𝑦𝜒) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7574imp 393 . . . . . . 7 ((𝜑 ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓)))
7675adantlr 686 . . . . . 6 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓)))
77 eqeq1 2774 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 = 𝑥𝑦 = 𝑥))
7877anbi1d 607 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ (𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
7978exbidv 2001 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
8079ad2antlr 698 . . . . . 6 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) ↔ ∃𝑥(𝑦 = 𝑥 ∧ (𝑋𝑥𝜓))))
8176, 80mpbird 247 . . . . 5 (((𝜑𝑧 = 𝑦) ∧ (𝑋𝑦𝜒)) → ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)))
8281ex 397 . . . 4 ((𝜑𝑧 = 𝑦) → ((𝑋𝑦𝜒) → ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))))
83 cnvcnvss 5730 . . . . 5 𝑦𝑦
8483a1i 11 . . . 4 (𝜑𝑦𝑦)
8530, 82, 84intabssd 38435 . . 3 (𝜑 {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} ⊆ {𝑦 ∣ (𝑋𝑦𝜒)})
86 vex 3352 . . . . 5 𝑧 ∈ V
8786a1i 11 . . . 4 (𝜑𝑧 ∈ V)
88 eqtr 2789 . . . . . . . 8 ((𝑦 = 𝑧𝑧 = 𝑥) → 𝑦 = 𝑥)
89 cnvss 5433 . . . . . . . . . . . 12 (𝑋𝑥𝑋𝑥)
90 sseq2 3774 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (𝑋𝑦𝑋𝑥))
9189, 90syl5ibr 236 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝑋𝑥𝑋𝑦))
9291adantl 467 . . . . . . . . . 10 ((𝜑𝑦 = 𝑥) → (𝑋𝑥𝑋𝑦))
93 clcnvlem.sub2 . . . . . . . . . 10 ((𝜑𝑦 = 𝑥) → (𝜓𝜒))
9492, 93anim12d 588 . . . . . . . . 9 ((𝜑𝑦 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒)))
9594ex 397 . . . . . . . 8 (𝜑 → (𝑦 = 𝑥 → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒))))
9688, 95syl5 34 . . . . . . 7 (𝜑 → ((𝑦 = 𝑧𝑧 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒))))
9796impl 443 . . . . . 6 (((𝜑𝑦 = 𝑧) ∧ 𝑧 = 𝑥) → ((𝑋𝑥𝜓) → (𝑋𝑦𝜒)))
9897expimpd 441 . . . . 5 ((𝜑𝑦 = 𝑧) → ((𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → (𝑋𝑦𝜒)))
9998exlimdv 2012 . . . 4 ((𝜑𝑦 = 𝑧) → (∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓)) → (𝑋𝑦𝜒)))
100 ssid 3771 . . . . 5 𝑧𝑧
101100a1i 11 . . . 4 (𝜑𝑧𝑧)
10287, 99, 101intabssd 38435 . . 3 (𝜑 {𝑦 ∣ (𝑋𝑦𝜒)} ⊆ {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))})
10385, 102eqssd 3767 . 2 (𝜑 {𝑧 ∣ ∃𝑥(𝑧 = 𝑥 ∧ (𝑋𝑥𝜓))} = {𝑦 ∣ (𝑋𝑦𝜒)})
1048, 26, 1033eqtrd 2808 1 (𝜑 {𝑥 ∣ (𝑋𝑥𝜓)} = {𝑦 ∣ (𝑋𝑦𝜒)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1630  wex 1851  wcel 2144  {cab 2756  {crab 3064  Vcvv 3349  cdif 3718  cun 3719  cin 3720  wss 3721  c0 4061  𝒫 cpw 4295   cint 4609   × cxp 5247  ccnv 5248  Rel wrel 5254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-int 4610  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fv 6039  df-1st 7314  df-2nd 7315
This theorem is referenced by:  cnvtrucl0  38450  cnvrcl0  38451  cnvtrcl0  38452
  Copyright terms: Public domain W3C validator