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

Theorem onfrALTlem5VD 41217
Description: Virtual deduction proof of onfrALTlem5 40874. 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. onfrALTlem5 40874 is onfrALTlem5VD 41217 without virtual deductions and was automatically derived from onfrALTlem5VD 41217.
1:: 𝑎 ∈ V
2:1: (𝑎𝑥) ∈ V
3:2: ([(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 𝑥) = ∅)
4:3: [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ ¬ (𝑎𝑥) = ∅)
5:: ((𝑎𝑥) ≠ ∅ ↔ ¬ (𝑎𝑥 ) = ∅)
6:4,5: [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎𝑥) ≠ ∅)
7:2: [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎𝑥) / 𝑏]¬ 𝑏 = ∅)
8:: (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
9:8: 𝑏(𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
10:2,9: ([(𝑎𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎𝑥) / 𝑏]¬ 𝑏 = ∅)
11:7,10: [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎𝑥) / 𝑏]𝑏 ≠ ∅)
12:6,11: ([(𝑎𝑥) / 𝑏]𝑏 ≠ ∅ ↔ ( 𝑎𝑥) ≠ ∅)
13:2: ([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥 ) ↔ (𝑎𝑥) ⊆ (𝑎𝑥))
14:12,13: (([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎 𝑥) ∧ [(𝑎𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎𝑥) ⊆ (𝑎 𝑥) ∧ (𝑎𝑥) ≠ ∅))
15:2: ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎 𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥) ∧ [(𝑎𝑥) / 𝑏]𝑏 ≠ ∅))
16:15,14: ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎 𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅))
17:2: (𝑎𝑥) / 𝑏(𝑏𝑦) = ( (𝑎𝑥) / 𝑏𝑏(𝑎𝑥) / 𝑏𝑦)
18:2: (𝑎𝑥) / 𝑏𝑏 = (𝑎𝑥)
19:2: (𝑎𝑥) / 𝑏𝑦 = 𝑦
20:18,19: ((𝑎𝑥) / 𝑏𝑏(𝑎 𝑥) / 𝑏𝑦) = ((𝑎𝑥) ∩ 𝑦)
21:17,20: (𝑎𝑥) / 𝑏(𝑏𝑦) = (( 𝑎𝑥) ∩ 𝑦)
22:2: ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ (𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏 ∅)
23:2: (𝑎𝑥) / 𝑏∅ = ∅
24:21,23: ((𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏∅ ↔ ((𝑎𝑥) ∩ 𝑦) = ∅)
25:22,24: ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ ((𝑎𝑥) ∩ 𝑦) = ∅)
26:2: ([(𝑎𝑥) / 𝑏]𝑦𝑏𝑦 (𝑎𝑥))
27:25,26: (([(𝑎𝑥) / 𝑏]𝑦𝑏[ (𝑎𝑥) / 𝑏](𝑏𝑦) = ∅) ↔ (𝑦 ∈ (𝑎𝑥) ∧ (( 𝑎𝑥) ∩ 𝑦) = ∅))
28:2: ([(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏 𝑦) = ∅) ↔ ([(𝑎𝑥) / 𝑏]𝑦𝑏[(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅))
29:27,28: ([(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
30:29: 𝑦([(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ (𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
31:30: (∃𝑦[(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦(𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) 𝑦) = ∅))
32:: (∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅ ))
33:31,32: (∃𝑦[(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅)
34:2: (∃𝑦[(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ [(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ ( 𝑏𝑦) = ∅))
35:33,34: ([(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦 ) = ∅)
36:: (∃𝑦𝑏(𝑏𝑦) = ∅ ↔ ∃𝑦 (𝑦𝑏 ∧ (𝑏𝑦) = ∅))
37:36: 𝑏(∃𝑦𝑏(𝑏𝑦) = ∅ ↔ 𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅))
38:2,37: ([(𝑎𝑥) / 𝑏]𝑦𝑏(𝑏 𝑦) = ∅ ↔ [(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅))
39:35,38: ([(𝑎𝑥) / 𝑏]𝑦𝑏(𝑏 𝑦) = ∅ ↔ ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅)
40:16,39: (([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏(𝑏 𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
41:2: ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏(𝑏𝑦) = ∅) ↔ ([(𝑎 𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏(𝑏𝑦) = ∅))
qed:40,41: ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏(𝑏𝑦) = ∅) ↔ (((𝑎 𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥 )((𝑎𝑥) ∩ 𝑦) = ∅))
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTlem5VD ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
Distinct variable groups:   𝑎,𝑏,𝑦   𝑥,𝑏,𝑦

Proof of Theorem onfrALTlem5VD
StepHypRef Expression
1 vex 3497 . . . 4 𝑎 ∈ V
21inex1 5220 . . 3 (𝑎𝑥) ∈ V
3 sbcimg 3819 . . 3 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅)))
42, 3e0a 41104 . 2 ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅))
5 sbcan 3820 . . . 4 ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥) ∧ [(𝑎𝑥) / 𝑏]𝑏 ≠ ∅))
6 sseq1 3991 . . . . . 6 (𝑏 = (𝑎𝑥) → (𝑏 ⊆ (𝑎𝑥) ↔ (𝑎𝑥) ⊆ (𝑎𝑥)))
72, 6sbcie 3811 . . . . 5 ([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥) ↔ (𝑎𝑥) ⊆ (𝑎𝑥))
8 df-ne 3017 . . . . . . 7 (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
98sbcbii 3828 . . . . . 6 ([(𝑎𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅)
10 sbcng 3818 . . . . . . . 8 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅ ↔ ¬ [(𝑎𝑥) / 𝑏]𝑏 = ∅))
1110bicomd 225 . . . . . . 7 ((𝑎𝑥) ∈ V → (¬ [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅))
122, 11e0a 41104 . . . . . 6 [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅)
13 eqsbc3 3816 . . . . . . . 8 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎𝑥) = ∅))
142, 13e0a 41104 . . . . . . 7 ([(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎𝑥) = ∅)
1514necon3bbii 3063 . . . . . 6 [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎𝑥) ≠ ∅)
169, 12, 153bitr2i 301 . . . . 5 ([(𝑎𝑥) / 𝑏]𝑏 ≠ ∅ ↔ (𝑎𝑥) ≠ ∅)
177, 16anbi12i 628 . . . 4 (([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥) ∧ [(𝑎𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅))
185, 17bitri 277 . . 3 ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅))
19 df-rex 3144 . . . . 5 (∃𝑦𝑏 (𝑏𝑦) = ∅ ↔ ∃𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅))
2019sbcbii 3828 . . . 4 ([(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅ ↔ [(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅))
21 sbcan 3820 . . . . . . 7 ([(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ([(𝑎𝑥) / 𝑏]𝑦𝑏[(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅))
22 sbcel2gv 3840 . . . . . . . . 9 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏]𝑦𝑏𝑦 ∈ (𝑎𝑥)))
232, 22e0a 41104 . . . . . . . 8 ([(𝑎𝑥) / 𝑏]𝑦𝑏𝑦 ∈ (𝑎𝑥))
24 sbceqg 4360 . . . . . . . . . 10 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ (𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏∅))
252, 24e0a 41104 . . . . . . . . 9 ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ (𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏∅)
26 csbin 4390 . . . . . . . . . . 11 (𝑎𝑥) / 𝑏(𝑏𝑦) = ((𝑎𝑥) / 𝑏𝑏(𝑎𝑥) / 𝑏𝑦)
27 csbvarg 4382 . . . . . . . . . . . . 13 ((𝑎𝑥) ∈ V → (𝑎𝑥) / 𝑏𝑏 = (𝑎𝑥))
282, 27e0a 41104 . . . . . . . . . . . 12 (𝑎𝑥) / 𝑏𝑏 = (𝑎𝑥)
29 csbconstg 3901 . . . . . . . . . . . . 13 ((𝑎𝑥) ∈ V → (𝑎𝑥) / 𝑏𝑦 = 𝑦)
302, 29e0a 41104 . . . . . . . . . . . 12 (𝑎𝑥) / 𝑏𝑦 = 𝑦
3128, 30ineq12i 4186 . . . . . . . . . . 11 ((𝑎𝑥) / 𝑏𝑏(𝑎𝑥) / 𝑏𝑦) = ((𝑎𝑥) ∩ 𝑦)
3226, 31eqtri 2844 . . . . . . . . . 10 (𝑎𝑥) / 𝑏(𝑏𝑦) = ((𝑎𝑥) ∩ 𝑦)
33 csb0 4358 . . . . . . . . . 10 (𝑎𝑥) / 𝑏∅ = ∅
3432, 33eqeq12i 2836 . . . . . . . . 9 ((𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏∅ ↔ ((𝑎𝑥) ∩ 𝑦) = ∅)
3525, 34bitri 277 . . . . . . . 8 ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ ((𝑎𝑥) ∩ 𝑦) = ∅)
3623, 35anbi12i 628 . . . . . . 7 (([(𝑎𝑥) / 𝑏]𝑦𝑏[(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅) ↔ (𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
3721, 36bitri 277 . . . . . 6 ([(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ (𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
3837exbii 1844 . . . . 5 (∃𝑦[(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦(𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
39 sbcex2 3833 . . . . 5 ([(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦[(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅))
40 df-rex 3144 . . . . 5 (∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
4138, 39, 403bitr4i 305 . . . 4 ([(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅)
4220, 41bitri 277 . . 3 ([(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅ ↔ ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅)
4318, 42imbi12i 353 . 2 (([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
444, 43bitri 277 1 ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398   = wceq 1533  wex 1776  wcel 2110  wne 3016  wrex 3139  Vcvv 3494  [wsbc 3771  csb 3882  cin 3934  wss 3935  c0 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-in 3942  df-ss 3951  df-nul 4291
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator