This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfac8clem

Description: Lemma for dfac8c . (Contributed by Mario Carneiro, 10-Jan-2013)

Ref Expression
Hypothesis dfac8clem.1 ⊢ 𝐹 = ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
Assertion dfac8clem ( 𝐴 ∈ 𝐵 → ( ∃ 𝑟 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 dfac8clem.1 ⊢ 𝐹 = ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
2 eldifsn ⊢ ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↔ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) )
3 elssuni ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ⊆ ∪ 𝐴 )
4 3 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑠 ⊆ ∪ 𝐴 )
5 simplr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑟 We ∪ 𝐴 )
6 vex ⊢ 𝑟 ∈ V
7 exse2 ⊢ ( 𝑟 ∈ V → 𝑟 Se ∪ 𝐴 )
8 6 7 mp1i ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑟 Se ∪ 𝐴 )
9 simprr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → 𝑠 ≠ ∅ )
10 wereu2 ⊢ ( ( ( 𝑟 We ∪ 𝐴 ∧ 𝑟 Se ∪ 𝐴 ) ∧ ( 𝑠 ⊆ ∪ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ∃! 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 )
11 5 8 4 9 10 syl22anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ∃! 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 )
12 riotacl ⊢ ( ∃! 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ 𝑠 )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ 𝑠 )
14 4 13 sseldd ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ ∪ 𝐴 )
15 2 14 sylan2b ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ) → ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ ∪ 𝐴 )
16 15 1 fmptd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → 𝐹 : ( 𝐴 ∖ { ∅ } ) ⟶ ∪ 𝐴 )
17 difexg ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∖ { ∅ } ) ∈ V )
18 17 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ( 𝐴 ∖ { ∅ } ) ∈ V )
19 uniexg ⊢ ( 𝐴 ∈ 𝐵 → ∪ 𝐴 ∈ V )
20 19 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∪ 𝐴 ∈ V )
21 fex2 ⊢ ( ( 𝐹 : ( 𝐴 ∖ { ∅ } ) ⟶ ∪ 𝐴 ∧ ( 𝐴 ∖ { ∅ } ) ∈ V ∧ ∪ 𝐴 ∈ V ) → 𝐹 ∈ V )
22 16 18 20 21 syl3anc ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → 𝐹 ∈ V )
23 riotaex ⊢ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ V
24 1 fvmpt2 ⊢ ( ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ∧ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) ∈ V ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
25 23 24 mpan2 ⊢ ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
26 2 25 sylbir ⊢ ( ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
27 26 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑠 ) = ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
28 27 13 eqeltrd ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑠 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 )
29 28 expr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
30 29 ralrimiva ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∀ 𝑠 ∈ 𝐴 ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
31 nfv ⊢ Ⅎ 𝑠 𝑧 ≠ ∅
32 nfmpt1 ⊢ Ⅎ 𝑠 ( 𝑠 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑎 ∈ 𝑠 ∀ 𝑏 ∈ 𝑠 ¬ 𝑏 𝑟 𝑎 ) )
33 1 32 nfcxfr ⊢ Ⅎ 𝑠 𝐹
34 nfcv ⊢ Ⅎ 𝑠 𝑧
35 33 34 nffv ⊢ Ⅎ 𝑠 ( 𝐹 ‘ 𝑧 )
36 35 nfel1 ⊢ Ⅎ 𝑠 ( 𝐹 ‘ 𝑧 ) ∈ 𝑧
37 31 36 nfim ⊢ Ⅎ 𝑠 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 )
38 nfv ⊢ Ⅎ 𝑧 ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 )
39 neeq1 ⊢ ( 𝑧 = 𝑠 → ( 𝑧 ≠ ∅ ↔ 𝑠 ≠ ∅ ) )
40 fveq2 ⊢ ( 𝑧 = 𝑠 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑠 ) )
41 id ⊢ ( 𝑧 = 𝑠 → 𝑧 = 𝑠 )
42 40 41 eleq12d ⊢ ( 𝑧 = 𝑠 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
43 39 42 imbi12d ⊢ ( 𝑧 = 𝑠 → ( ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) ) )
44 37 38 43 cbvralw ⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑠 ∈ 𝐴 ( 𝑠 ≠ ∅ → ( 𝐹 ‘ 𝑠 ) ∈ 𝑠 ) )
45 30 44 sylibr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
46 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
47 46 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
48 47 imbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ) )
49 48 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ) )
50 22 45 49 spcedv ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑟 We ∪ 𝐴 ) → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
51 50 ex ⊢ ( 𝐴 ∈ 𝐵 → ( 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
52 51 exlimdv ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑟 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )