Step |
Hyp |
Ref |
Expression |
1 |
|
fneq2 |
⊢ ( 𝑤 = ∅ → ( 𝑓 Fn 𝑤 ↔ 𝑓 Fn ∅ ) ) |
2 |
|
raleq |
⊢ ( 𝑤 = ∅ → ( ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
3 |
1 2
|
anbi12d |
⊢ ( 𝑤 = ∅ → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
4 |
3
|
exbidv |
⊢ ( 𝑤 = ∅ → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
5 |
|
fneq2 |
⊢ ( 𝑤 = 𝑦 → ( 𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝑦 ) ) |
6 |
|
raleq |
⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
7 |
5 6
|
anbi12d |
⊢ ( 𝑤 = 𝑦 → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
8 |
7
|
exbidv |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
9 |
|
fneq2 |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑓 Fn 𝑤 ↔ 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ) ) |
10 |
|
raleq |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
11 |
9 10
|
anbi12d |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
12 |
11
|
exbidv |
⊢ ( 𝑤 = ( 𝑦 ∪ { 𝑧 } ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
13 |
|
fneq2 |
⊢ ( 𝑤 = 𝐴 → ( 𝑓 Fn 𝑤 ↔ 𝑓 Fn 𝐴 ) ) |
14 |
|
raleq |
⊢ ( 𝑤 = 𝐴 → ( ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
15 |
13 14
|
anbi12d |
⊢ ( 𝑤 = 𝐴 → ( ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
16 |
15
|
exbidv |
⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑓 ( 𝑓 Fn 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
17 |
|
0ex |
⊢ ∅ ∈ V |
18 |
|
fneq1 |
⊢ ( 𝑓 = ∅ → ( 𝑓 Fn ∅ ↔ ∅ Fn ∅ ) ) |
19 |
|
eqid |
⊢ ∅ = ∅ |
20 |
|
fn0 |
⊢ ( ∅ Fn ∅ ↔ ∅ = ∅ ) |
21 |
19 20
|
mpbir |
⊢ ∅ Fn ∅ |
22 |
17 18 21
|
ceqsexv2d |
⊢ ∃ 𝑓 𝑓 Fn ∅ |
23 |
|
ral0 |
⊢ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) |
24 |
22 23
|
exan |
⊢ ∃ 𝑓 ( 𝑓 Fn ∅ ∧ ∀ 𝑥 ∈ ∅ ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
25 |
|
dffn2 |
⊢ ( 𝑓 Fn 𝑦 ↔ 𝑓 : 𝑦 ⟶ V ) |
26 |
25
|
biimpi |
⊢ ( 𝑓 Fn 𝑦 → 𝑓 : 𝑦 ⟶ V ) |
27 |
26
|
ad2antrl |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → 𝑓 : 𝑦 ⟶ V ) |
28 |
|
vex |
⊢ 𝑧 ∈ V |
29 |
28
|
a1i |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → 𝑧 ∈ V ) |
30 |
|
simpllr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ¬ 𝑧 ∈ 𝑦 ) |
31 |
|
vex |
⊢ 𝑤 ∈ V |
32 |
31
|
a1i |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → 𝑤 ∈ V ) |
33 |
|
fsnunf |
⊢ ( ( 𝑓 : 𝑦 ⟶ V ∧ ( 𝑧 ∈ V ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑤 ∈ V ) → ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V ) |
34 |
27 29 30 32 33
|
syl121anc |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V ) |
35 |
|
dffn2 |
⊢ ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V ) |
36 |
34 35
|
sylibr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ) |
37 |
|
simplr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → 𝑧 = ∅ ) |
38 |
|
simprr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
39 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) |
40 |
|
nfra1 |
⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) |
41 |
39 40
|
nfan |
⊢ Ⅎ 𝑥 ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
42 |
|
simpr |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝑦 ) |
43 |
|
simpllr |
⊢ ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ¬ 𝑧 ∈ 𝑦 ) |
44 |
43
|
adantr |
⊢ ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ¬ 𝑧 ∈ 𝑦 ) |
45 |
44
|
adantr |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑦 ) |
46 |
42 45
|
jca |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦 ) ) |
47 |
|
nelne2 |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦 ) → 𝑥 ≠ 𝑧 ) |
48 |
47
|
necomd |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦 ) → 𝑧 ≠ 𝑥 ) |
49 |
46 48
|
syl |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → 𝑧 ≠ 𝑥 ) |
50 |
|
fvunsn |
⊢ ( 𝑧 ≠ 𝑥 → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) ) |
51 |
49 50
|
syl |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) ) |
52 |
|
simpllr |
⊢ ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
53 |
52
|
adantr |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
54 |
|
simplr |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ≠ ∅ ) |
55 |
|
neeq1 |
⊢ ( 𝑢 = 𝑥 → ( 𝑢 ≠ ∅ ↔ 𝑥 ≠ ∅ ) ) |
56 |
|
fveq2 |
⊢ ( 𝑢 = 𝑥 → ( 𝑓 ‘ 𝑢 ) = ( 𝑓 ‘ 𝑥 ) ) |
57 |
56
|
eleq1d |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝑢 ) ) |
58 |
|
eleq2w |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑢 ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
59 |
57 58
|
bitrd |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
60 |
55 59
|
imbi12d |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ≠ ∅ → ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ↔ ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
61 |
60
|
cbvralvw |
⊢ ( ∀ 𝑢 ∈ 𝑦 ( 𝑢 ≠ ∅ → ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
62 |
60
|
rspcv |
⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑢 ∈ 𝑦 ( 𝑢 ≠ ∅ → ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) → ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
63 |
61 62
|
syl5bir |
⊢ ( 𝑥 ∈ 𝑦 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) → ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
64 |
42 53 54 63
|
syl3c |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) |
65 |
51 64
|
eqeltrd |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) |
66 |
|
simp-4l |
⊢ ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑧 = ∅ ) |
67 |
66
|
adantr |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑧 = ∅ ) |
68 |
|
simpr |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 ∈ { 𝑧 } ) |
69 |
|
simplr |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 ≠ ∅ ) |
70 |
|
elsni |
⊢ ( 𝑥 ∈ { 𝑧 } → 𝑥 = 𝑧 ) |
71 |
70
|
3ad2ant2 |
⊢ ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑥 = 𝑧 ) |
72 |
|
simp1 |
⊢ ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑧 = ∅ ) |
73 |
71 72
|
eqtrd |
⊢ ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑥 = ∅ ) |
74 |
|
simp3 |
⊢ ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → 𝑥 ≠ ∅ ) |
75 |
73 74
|
pm2.21ddne |
⊢ ( ( 𝑧 = ∅ ∧ 𝑥 ∈ { 𝑧 } ∧ 𝑥 ≠ ∅ ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) |
76 |
67 68 69 75
|
syl3anc |
⊢ ( ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) |
77 |
|
simplr |
⊢ ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) |
78 |
|
elun |
⊢ ( 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑥 ∈ { 𝑧 } ) ) |
79 |
77 78
|
sylib |
⊢ ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( 𝑥 ∈ 𝑦 ∨ 𝑥 ∈ { 𝑧 } ) ) |
80 |
65 76 79
|
mpjaodan |
⊢ ( ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) |
81 |
80
|
ex |
⊢ ( ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
82 |
81
|
ex |
⊢ ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ( 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
83 |
41 82
|
ralrimi |
⊢ ( ( ( 𝑧 = ∅ ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
84 |
37 30 38 83
|
syl21anc |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
85 |
36 84
|
jca |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
86 |
85
|
ex |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) → ( ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
87 |
86
|
eximdv |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
88 |
|
vex |
⊢ 𝑓 ∈ V |
89 |
|
snex |
⊢ { 〈 𝑧 , 𝑤 〉 } ∈ V |
90 |
88 89
|
unex |
⊢ ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ∈ V |
91 |
|
fneq1 |
⊢ ( 𝑔 = ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) → ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ↔ ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ) ) |
92 |
|
fveq1 |
⊢ ( 𝑔 = ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) → ( 𝑔 ‘ 𝑥 ) = ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ) |
93 |
92
|
eleq1d |
⊢ ( 𝑔 = ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ↔ ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
94 |
93
|
imbi2d |
⊢ ( 𝑔 = ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) → ( ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
95 |
94
|
ralbidv |
⊢ ( 𝑔 = ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
96 |
91 95
|
anbi12d |
⊢ ( 𝑔 = ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) → ( ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
97 |
90 96
|
spcev |
⊢ ( ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
98 |
97
|
eximi |
⊢ ( ∃ 𝑓 ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
99 |
87 98
|
syl6 |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
100 |
|
ax5e |
⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
101 |
99 100
|
syl6 |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
102 |
101
|
imp |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ 𝑧 = ∅ ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
103 |
102
|
an32s |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ 𝑧 = ∅ ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
104 |
|
fneq1 |
⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ) ) |
105 |
|
fveq1 |
⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) |
106 |
105
|
eleq1d |
⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ↔ ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) |
107 |
106
|
imbi2d |
⊢ ( 𝑓 = 𝑔 → ( ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
108 |
107
|
ralbidv |
⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
109 |
104 108
|
anbi12d |
⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
110 |
109
|
cbvexvw |
⊢ ( ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
111 |
103 110
|
sylibr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ 𝑧 = ∅ ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
112 |
|
simpllr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ¬ 𝑧 ∈ 𝑦 ) |
113 |
|
simpr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ¬ 𝑧 = ∅ ) |
114 |
|
neq0 |
⊢ ( ¬ 𝑧 = ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑧 ) |
115 |
113 114
|
sylib |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ∃ 𝑤 𝑤 ∈ 𝑧 ) |
116 |
|
simplr |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
117 |
115 116
|
jca |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
118 |
112 117
|
jca |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ( ¬ 𝑧 ∈ 𝑦 ∧ ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ) |
119 |
|
exdistrv |
⊢ ( ∃ 𝑤 ∃ 𝑓 ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ↔ ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
120 |
|
simprrl |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑓 Fn 𝑦 ) |
121 |
120 25
|
sylib |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑓 : 𝑦 ⟶ V ) |
122 |
28
|
a1i |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑧 ∈ V ) |
123 |
|
simpl |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ¬ 𝑧 ∈ 𝑦 ) |
124 |
31
|
a1i |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → 𝑤 ∈ V ) |
125 |
121 122 123 124 33
|
syl121anc |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ V ) |
126 |
125 35
|
sylibr |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ) |
127 |
|
nfv |
⊢ Ⅎ 𝑥 ¬ 𝑧 ∈ 𝑦 |
128 |
|
nfv |
⊢ Ⅎ 𝑥 𝑤 ∈ 𝑧 |
129 |
|
nfv |
⊢ Ⅎ 𝑥 𝑓 Fn 𝑦 |
130 |
129 40
|
nfan |
⊢ Ⅎ 𝑥 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
131 |
128 130
|
nfan |
⊢ Ⅎ 𝑥 ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
132 |
127 131
|
nfan |
⊢ Ⅎ 𝑥 ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
133 |
|
simpr |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝑦 ) |
134 |
|
simp-4l |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑦 ) |
135 |
133 134
|
jca |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦 ) ) |
136 |
48 50
|
syl |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) ) |
137 |
135 136
|
syl |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) ) |
138 |
|
simprrr |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
139 |
138
|
ad5ant12 |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
140 |
|
simplr |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ≠ ∅ ) |
141 |
133 139 140 63
|
syl3c |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) |
142 |
137 141
|
eqeltrd |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) |
143 |
|
simplrl |
⊢ ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑤 ∈ 𝑧 ) |
144 |
143
|
adantr |
⊢ ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑤 ∈ 𝑧 ) |
145 |
144
|
adantr |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑤 ∈ 𝑧 ) |
146 |
|
simpr |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 ∈ { 𝑧 } ) |
147 |
146 70
|
syl |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑥 = 𝑧 ) |
148 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) = ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑧 ) ) |
149 |
147 148
|
syl |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) = ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑧 ) ) |
150 |
28
|
a1i |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑧 ∈ V ) |
151 |
31
|
a1i |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑤 ∈ V ) |
152 |
|
simp-4l |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ¬ 𝑧 ∈ 𝑦 ) |
153 |
120
|
ad5ant12 |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → 𝑓 Fn 𝑦 ) |
154 |
153
|
fndmd |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → dom 𝑓 = 𝑦 ) |
155 |
152 154
|
neleqtrrd |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ¬ 𝑧 ∈ dom 𝑓 ) |
156 |
|
fsnunfv |
⊢ ( ( 𝑧 ∈ V ∧ 𝑤 ∈ V ∧ ¬ 𝑧 ∈ dom 𝑓 ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑧 ) = 𝑤 ) |
157 |
150 151 155 156
|
syl3anc |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑧 ) = 𝑤 ) |
158 |
149 157
|
eqtrd |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) = 𝑤 ) |
159 |
145 158 147
|
3eltr4d |
⊢ ( ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑥 ∈ { 𝑧 } ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) |
160 |
|
simplr |
⊢ ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) |
161 |
160 78
|
sylib |
⊢ ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( 𝑥 ∈ 𝑦 ∨ 𝑥 ∈ { 𝑧 } ) ) |
162 |
142 159 161
|
mpjaodan |
⊢ ( ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) ∧ 𝑥 ≠ ∅ ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) |
163 |
162
|
ex |
⊢ ( ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) ∧ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
164 |
163
|
ex |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ( 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
165 |
132 164
|
ralrimi |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
166 |
126 165
|
jca |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( ( 𝑓 ∪ { 〈 𝑧 , 𝑤 〉 } ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
167 |
166 97
|
syl |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
168 |
167
|
ex |
⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
169 |
168
|
2eximdv |
⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ∃ 𝑤 ∃ 𝑓 ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
170 |
119 169
|
syl5bir |
⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
171 |
170
|
imp |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
172 |
100
|
exlimiv |
⊢ ( ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
173 |
171 172
|
syl |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑔 ( 𝑔 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
174 |
173 110
|
sylibr |
⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( ∃ 𝑤 𝑤 ∈ 𝑧 ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
175 |
118 174
|
syl |
⊢ ( ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ∧ ¬ 𝑧 = ∅ ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
176 |
111 175
|
pm2.61dan |
⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
177 |
176
|
ex |
⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ( 𝑓 Fn ( 𝑦 ∪ { 𝑧 } ) ∧ ∀ 𝑥 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) ) |
178 |
4 8 12 16 24 177
|
findcard2s |
⊢ ( 𝐴 ∈ Fin → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |