Metamath Proof Explorer

Theorem onfrALTlem5

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem5 ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑎 ∈ V
2 1 inex1 ⊢ ( 𝑎 ∩ 𝑥 ) ∈ V
3 sbcimg ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) )
4 2 3 ax-mp ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) )
5 sbcan ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ) )
6 sseq1 ⊢ ( 𝑏 = ( 𝑎 ∩ 𝑥 ) → ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ↔ ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ) )
7 2 6 sbcie ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ↔ ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) )
8 df-ne ⊢ ( 𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅ )
9 8 sbcbii ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ )
10 sbcng ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ ↔ ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ) )
11 10 bicomd ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ ) )
12 2 11 ax-mp ⊢ ( ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ¬ 𝑏 = ∅ )
13 eqsbc3 ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ ( 𝑎 ∩ 𝑥 ) = ∅ ) )
14 2 13 ax-mp ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ ( 𝑎 ∩ 𝑥 ) = ∅ )
15 14 necon3bbii ⊢ ( ¬ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 = ∅ ↔ ( 𝑎 ∩ 𝑥 ) ≠ ∅ )
16 9 12 15 3bitr2i ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ↔ ( 𝑎 ∩ 𝑥 ) ≠ ∅ )
17 7 16 anbi12i ⊢ ( ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑏 ≠ ∅ ) ↔ ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) )
18 5 17 bitri ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) ↔ ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) )
19 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) )
20 19 sbcbii ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ↔ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) )
21 sbcan ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ) )
22 sbcel2gv ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ) )
23 2 22 ax-mp ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ↔ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) )
24 sbceqg ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ ) )
25 2 24 ax-mp ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ )
26 csbin ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ( ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 ∩ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 )
27 csbvarg ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 = ( 𝑎 ∩ 𝑥 ) )
28 2 27 ax-mp ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 = ( 𝑎 ∩ 𝑥 )
29 csbconstg ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 = 𝑦 )
30 2 29 ax-mp ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 = 𝑦
31 28 30 ineq12i ⊢ ( ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑏 ∩ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ 𝑦 ) = ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 )
32 26 31 eqtri ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 )
33 csb0 ⊢ ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ = ∅
34 32 33 eqeq12i ⊢ ( ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ( 𝑏 ∩ 𝑦 ) = ⦋ ( 𝑎 ∩ 𝑥 ) / 𝑏 ⦌ ∅ ↔ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )
35 25 34 bitri ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )
36 23 35 anbi12i ⊢ ( ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] 𝑦 ∈ 𝑏 ∧ [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
37 21 36 bitri ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
38 37 exbii ⊢ ( ∃ 𝑦 [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
39 sbcex2 ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑦 [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) )
40 df-rex ⊢ ( ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
41 38 39 40 3bitr4i ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ( 𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )
42 20 41 bitri ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )
43 18 42 imbi12i ⊢ ( ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
44 4 43 bitri ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )