Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbrngVD Structured version   Visualization version   GIF version

Theorem csbrngVD 44572
Description: Virtual deduction proof of csbrn 6214. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbrn 6214 is csbrngVD 44572 without virtual deductions and was automatically derived from csbrngVD 44572.
1:: (   𝐴𝑉   ▶   𝐴𝑉   )
2:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤   ,   𝑦 𝐵𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
3:1: (   𝐴𝑉   ▶   𝐴 / 𝑥𝑤   ,   𝑦⟩ = 𝑤, 𝑦   )
4:3: (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑤   ,   𝑦 𝐴 / 𝑥𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
5:2,4: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤   ,   𝑦 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
6:5: (   𝐴𝑉   ▶   𝑤([𝐴 / 𝑥]𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
7:6: (   𝐴𝑉   ▶   (∃𝑤[𝐴 / 𝑥]𝑤   ,    𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
8:1: (   𝐴𝑉   ▶   (∃𝑤[𝐴 / 𝑥]𝑤   ,    𝑦⟩ ∈ 𝐵[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵)   )
9:7,8: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝑤    ,   𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
10:9: (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥]𝑤 𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
11:10: (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑤 𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}   )
12:1: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦 ∣ ∃𝑤 𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵}   )
13:11,12: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦 ∣ ∃𝑤 𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}   )
14:: ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤   ,   𝑦⟩ ∈ 𝐵}
15:14: 𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤   ,   𝑦 𝐵}
16:1,15: (   𝐴𝑉   ▶   𝐴 / 𝑥ran 𝐵 = 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵}   )
17:13,16: (   𝐴𝑉   ▶   𝐴 / 𝑥ran 𝐵 = {𝑦 𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}   )
18:: ran 𝐴 / 𝑥𝐵 = {𝑦 ∣ ∃𝑤𝑤    ,   𝑦⟩ ∈ 𝐴 / 𝑥𝐵}
19:17,18: (   𝐴𝑉   ▶   𝐴 / 𝑥ran 𝐵 = ran 𝐴 / 𝑥𝐵   )
qed:19: (𝐴𝑉𝐴 / 𝑥ran 𝐵 = ran 𝐴 / 𝑥𝐵)
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbrngVD (𝐴𝑉𝐴 / 𝑥ran 𝐵 = ran 𝐴 / 𝑥𝐵)

Proof of Theorem csbrngVD
Dummy variables 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 44250 . . . . . . . . . . . 12 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbcel12 4413 . . . . . . . . . . . . 13 ([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)
32a1i 11 . . . . . . . . . . . 12 (𝐴𝑉 → ([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵))
41, 3e1a 44303 . . . . . . . . . . 11 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
5 csbconstg 3911 . . . . . . . . . . . . 13 (𝐴𝑉𝐴 / 𝑥𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩)
61, 5e1a 44303 . . . . . . . . . . . 12 (   𝐴𝑉   ▶   𝐴 / 𝑥𝑤, 𝑦⟩ = ⟨𝑤, 𝑦   )
7 eleq1 2814 . . . . . . . . . . . 12 (𝐴 / 𝑥𝑤, 𝑦⟩ = ⟨𝑤, 𝑦⟩ → (𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵))
86, 7e1a 44303 . . . . . . . . . . 11 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
9 bibi1 350 . . . . . . . . . . . 12 (([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) ↔ (𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)))
109biimprd 247 . . . . . . . . . . 11 (([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) → ((𝐴 / 𝑥𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) → ([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)))
114, 8, 10e11 44364 . . . . . . . . . 10 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
1211gen11 44292 . . . . . . . . 9 (   𝐴𝑉   ▶   𝑤([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
13 exbi 1842 . . . . . . . . 9 (∀𝑤([𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ⟨𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) → (∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵))
1412, 13e1a 44303 . . . . . . . 8 (   𝐴𝑉   ▶   (∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
15 sbcex2 3841 . . . . . . . . . . 11 ([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵)
1615a1i 11 . . . . . . . . . 10 (𝐴𝑉 → ([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵))
1716bicomd 222 . . . . . . . . 9 (𝐴𝑉 → (∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵))
181, 17e1a 44303 . . . . . . . 8 (   𝐴𝑉   ▶   (∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵)   )
19 bitr3 351 . . . . . . . . 9 ((∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵) → ((∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) → ([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)))
2019com12 32 . . . . . . . 8 ((∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) → ((∃𝑤[𝐴 / 𝑥]𝑤, 𝑦⟩ ∈ 𝐵[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵) → ([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)))
2114, 18, 20e11 44364 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
2221gen11 44292 . . . . . 6 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵)   )
23 abbib 2798 . . . . . . 7 ({𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} ↔ ∀𝑦([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵))
2423biimpri 227 . . . . . 6 (∀𝑦([𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵 ↔ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵) → {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵})
2522, 24e1a 44303 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}   )
26 csbab 4442 . . . . . . 7 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵}
2726a1i 11 . . . . . 6 (𝐴𝑉𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵})
281, 27e1a 44303 . . . . 5 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵}   )
29 eqeq2 2738 . . . . . 6 ({𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵} ↔ 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}))
3029biimpd 228 . . . . 5 ({𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦[𝐴 / 𝑥]𝑤𝑤, 𝑦⟩ ∈ 𝐵} → 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}))
3125, 28, 30e11 44364 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}   )
32 dfrn3 5896 . . . . . 6 ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵}
3332ax-gen 1790 . . . . 5 𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵}
34 csbeq2 3897 . . . . . 6 (∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} → 𝐴 / 𝑥ran 𝐵 = 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵})
3534a1i 11 . . . . 5 (𝐴𝑉 → (∀𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} → 𝐴 / 𝑥ran 𝐵 = 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵}))
361, 33, 35e10 44370 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥ran 𝐵 = 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵}   )
37 eqeq2 2738 . . . . 5 (𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥ran 𝐵 = 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} ↔ 𝐴 / 𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}))
3837biimpd 228 . . . 4 (𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥ran 𝐵 = 𝐴 / 𝑥{𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐵} → 𝐴 / 𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}))
3931, 36, 38e11 44364 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}   )
40 dfrn3 5896 . . 3 ran 𝐴 / 𝑥𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}
41 eqeq2 2738 . . . 4 (ran 𝐴 / 𝑥𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥ran 𝐵 = ran 𝐴 / 𝑥𝐵𝐴 / 𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵}))
4241biimprcd 249 . . 3 (𝐴 / 𝑥ran 𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} → (ran 𝐴 / 𝑥𝐵 = {𝑦 ∣ ∃𝑤𝑤, 𝑦⟩ ∈ 𝐴 / 𝑥𝐵} → 𝐴 / 𝑥ran 𝐵 = ran 𝐴 / 𝑥𝐵))
4339, 40, 42e10 44370 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥ran 𝐵 = ran 𝐴 / 𝑥𝐵   )
4443in1 44247 1 (𝐴𝑉𝐴 / 𝑥ran 𝐵 = ran 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1532   = wceq 1534  wex 1774  wcel 2099  {cab 2703  [wsbc 3776  csb 3892  cop 4639  ran crn 5683
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-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216  df-cnv 5690  df-dm 5692  df-rn 5693  df-vd1 44246
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator