ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ac6sfi GIF version

Theorem ac6sfi 6897
Description: Existence of a choice function for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
Hypothesis
Ref Expression
ac6sfi.1 (𝑦 = (π‘“β€˜π‘₯) β†’ (πœ‘ ↔ πœ“))
Assertion
Ref Expression
ac6sfi ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘) β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))
Distinct variable groups:   π‘₯,𝑓,𝐴   𝑦,𝑓,𝐡,π‘₯   πœ‘,𝑓   πœ“,𝑦
Allowed substitution hints:   πœ‘(π‘₯,𝑦)   πœ“(π‘₯,𝑓)   𝐴(𝑦)

Proof of Theorem ac6sfi
Dummy variables 𝑒 𝑀 𝑧 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 2672 . . . 4 (𝑒 = βˆ… β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘))
2 feq2 5349 . . . . . 6 (𝑒 = βˆ… β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:βˆ…βŸΆπ΅))
3 raleq 2672 . . . . . 6 (𝑒 = βˆ… β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ βˆ… πœ“))
42, 3anbi12d 473 . . . . 5 (𝑒 = βˆ… β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“)))
54exbidv 1825 . . . 4 (𝑒 = βˆ… β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“)))
61, 5imbi12d 234 . . 3 (𝑒 = βˆ… β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))))
7 raleq 2672 . . . 4 (𝑒 = 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
8 feq2 5349 . . . . . 6 (𝑒 = 𝑀 β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:π‘€βŸΆπ΅))
9 raleq 2672 . . . . . 6 (𝑒 = 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 πœ“))
108, 9anbi12d 473 . . . . 5 (𝑒 = 𝑀 β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
1110exbidv 1825 . . . 4 (𝑒 = 𝑀 β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
127, 11imbi12d 234 . . 3 (𝑒 = 𝑀 β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“))))
13 raleq 2672 . . . 4 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘))
14 feq2 5349 . . . . . . 7 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡))
15 raleq 2672 . . . . . . 7 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“))
1614, 15anbi12d 473 . . . . . 6 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“)))
1716exbidv 1825 . . . . 5 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“)))
18 feq1 5348 . . . . . . 7 (𝑓 = 𝑔 β†’ (𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ↔ 𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡))
19 vex 2740 . . . . . . . . . . 11 𝑓 ∈ V
20 vex 2740 . . . . . . . . . . 11 π‘₯ ∈ V
2119, 20fvex 5535 . . . . . . . . . 10 (π‘“β€˜π‘₯) ∈ V
22 ac6sfi.1 . . . . . . . . . 10 (𝑦 = (π‘“β€˜π‘₯) β†’ (πœ‘ ↔ πœ“))
2321, 22sbcie 2997 . . . . . . . . 9 ([(π‘“β€˜π‘₯) / 𝑦]πœ‘ ↔ πœ“)
24 fveq1 5514 . . . . . . . . . 10 (𝑓 = 𝑔 β†’ (π‘“β€˜π‘₯) = (π‘”β€˜π‘₯))
2524sbceq1d 2967 . . . . . . . . 9 (𝑓 = 𝑔 β†’ ([(π‘“β€˜π‘₯) / 𝑦]πœ‘ ↔ [(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2623, 25bitr3id 194 . . . . . . . 8 (𝑓 = 𝑔 β†’ (πœ“ ↔ [(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2726ralbidv 2477 . . . . . . 7 (𝑓 = 𝑔 β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
2818, 27anbi12d 473 . . . . . 6 (𝑓 = 𝑔 β†’ ((𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“) ↔ (𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
2928cbvexv 1918 . . . . 5 (βˆƒπ‘“(𝑓:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})πœ“) ↔ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
3017, 29bitrdi 196 . . . 4 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
3113, 30imbi12d 234 . . 3 (𝑒 = (𝑀 βˆͺ {𝑧}) β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
32 raleq 2672 . . . 4 (𝑒 = 𝐴 β†’ (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
33 feq2 5349 . . . . . 6 (𝑒 = 𝐴 β†’ (𝑓:π‘’βŸΆπ΅ ↔ 𝑓:𝐴⟢𝐡))
34 raleq 2672 . . . . . 6 (𝑒 = 𝐴 β†’ (βˆ€π‘₯ ∈ 𝑒 πœ“ ↔ βˆ€π‘₯ ∈ 𝐴 πœ“))
3533, 34anbi12d 473 . . . . 5 (𝑒 = 𝐴 β†’ ((𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ (𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
3635exbidv 1825 . . . 4 (𝑒 = 𝐴 β†’ (βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“) ↔ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
3732, 36imbi12d 234 . . 3 (𝑒 = 𝐴 β†’ ((βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘’βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑒 πœ“)) ↔ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))))
38 f0 5406 . . . 4 βˆ…:βˆ…βŸΆπ΅
39 0ex 4130 . . . . 5 βˆ… ∈ V
40 ral0 3524 . . . . . . 7 βˆ€π‘₯ ∈ βˆ… πœ“
4140biantru 302 . . . . . 6 (𝑓:βˆ…βŸΆπ΅ ↔ (𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
42 feq1 5348 . . . . . 6 (𝑓 = βˆ… β†’ (𝑓:βˆ…βŸΆπ΅ ↔ βˆ…:βˆ…βŸΆπ΅))
4341, 42bitr3id 194 . . . . 5 (𝑓 = βˆ… β†’ ((𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“) ↔ βˆ…:βˆ…βŸΆπ΅))
4439, 43spcev 2832 . . . 4 (βˆ…:βˆ…βŸΆπ΅ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
4538, 44mp1i 10 . . 3 (βˆ€π‘₯ ∈ βˆ… βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:βˆ…βŸΆπ΅ ∧ βˆ€π‘₯ ∈ βˆ… πœ“))
46 ssun1 3298 . . . . . . 7 𝑀 βŠ† (𝑀 βˆͺ {𝑧})
47 ssralv 3219 . . . . . . 7 (𝑀 βŠ† (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘))
4846, 47ax-mp 5 . . . . . 6 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘)
4948imim1i 60 . . . . 5 ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)))
50 ssun2 3299 . . . . . . . . 9 {𝑧} βŠ† (𝑀 βˆͺ {𝑧})
51 ssralv 3219 . . . . . . . . 9 ({𝑧} βŠ† (𝑀 βˆͺ {𝑧}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘))
5250, 51ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘)
53 vex 2740 . . . . . . . . . 10 𝑧 ∈ V
54 ralsnsg 3629 . . . . . . . . . 10 (𝑧 ∈ V β†’ (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ [𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘))
5553, 54ax-mp 5 . . . . . . . . 9 (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ [𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘)
56 sbcrex 3042 . . . . . . . . 9 ([𝑧 / π‘₯]βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
5755, 56bitri 184 . . . . . . . 8 (βˆ€π‘₯ ∈ {𝑧}βˆƒπ‘¦ ∈ 𝐡 πœ‘ ↔ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
5852, 57sylib 122 . . . . . . 7 (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘)
59 nfv 1528 . . . . . . . 8 Ⅎ𝑦 Β¬ 𝑧 ∈ 𝑀
60 nfv 1528 . . . . . . . . 9 β„²π‘¦βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)
61 nfv 1528 . . . . . . . . . . 11 Ⅎ𝑦 𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡
62 nfcv 2319 . . . . . . . . . . . 12 Ⅎ𝑦(𝑀 βˆͺ {𝑧})
63 nfsbc1v 2981 . . . . . . . . . . . 12 Ⅎ𝑦[(π‘”β€˜π‘₯) / 𝑦]πœ‘
6462, 63nfralxy 2515 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘
6561, 64nfan 1565 . . . . . . . . . 10 Ⅎ𝑦(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)
6665nfex 1637 . . . . . . . . 9 β„²π‘¦βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)
6760, 66nfim 1572 . . . . . . . 8 Ⅎ𝑦(βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
68 simprl 529 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑓:π‘€βŸΆπ΅)
69 vex 2740 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
7053, 69f1osn 5501 . . . . . . . . . . . . . . 15 {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}–1-1-ontoβ†’{𝑦}
71 f1of 5461 . . . . . . . . . . . . . . 15 ({βŸ¨π‘§, π‘¦βŸ©}:{𝑧}–1-1-ontoβ†’{𝑦} β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢{𝑦})
7270, 71mp1i 10 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢{𝑦})
73 simpl2 1001 . . . . . . . . . . . . . . 15 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑦 ∈ 𝐡)
7473snssd 3737 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {𝑦} βŠ† 𝐡)
7572, 74fssd 5378 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢𝐡)
76 simpl1 1000 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ Β¬ 𝑧 ∈ 𝑀)
77 disjsn 3654 . . . . . . . . . . . . . 14 ((𝑀 ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ 𝑀)
7876, 77sylibr 134 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (𝑀 ∩ {𝑧}) = βˆ…)
79 fun2 5389 . . . . . . . . . . . . 13 (((𝑓:π‘€βŸΆπ΅ ∧ {βŸ¨π‘§, π‘¦βŸ©}:{𝑧}⟢𝐡) ∧ (𝑀 ∩ {𝑧}) = βˆ…) β†’ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡)
8068, 75, 78, 79syl21anc 1237 . . . . . . . . . . . 12 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡)
81 simprr 531 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ 𝑀 πœ“)
82 eleq1a 2249 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ 𝑀 β†’ (𝑧 = π‘₯ β†’ 𝑧 ∈ 𝑀))
8382necon3bd 2390 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝑀 β†’ (Β¬ 𝑧 ∈ 𝑀 β†’ 𝑧 β‰  π‘₯))
8483impcom 125 . . . . . . . . . . . . . . . . 17 ((Β¬ 𝑧 ∈ 𝑀 ∧ π‘₯ ∈ 𝑀) β†’ 𝑧 β‰  π‘₯)
85 fvunsng 5710 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ V ∧ 𝑧 β‰  π‘₯) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯))
8620, 85mpan 424 . . . . . . . . . . . . . . . . 17 (𝑧 β‰  π‘₯ β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯))
87 dfsbcq 2964 . . . . . . . . . . . . . . . . . 18 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯) β†’ ([((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘ ↔ [(π‘“β€˜π‘₯) / 𝑦]πœ‘))
8887, 23bitr2di 197 . . . . . . . . . . . . . . . . 17 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = (π‘“β€˜π‘₯) β†’ (πœ“ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
8984, 86, 883syl 17 . . . . . . . . . . . . . . . 16 ((Β¬ 𝑧 ∈ 𝑀 ∧ π‘₯ ∈ 𝑀) β†’ (πœ“ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9089ralbidva 2473 . . . . . . . . . . . . . . 15 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆ€π‘₯ ∈ 𝑀 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9176, 90syl 14 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ 𝑀 πœ“ ↔ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
9281, 91mpbid 147 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
93 simpl3 1002 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ [𝑧 / π‘₯]πœ‘)
94 ffun 5368 . . . . . . . . . . . . . . . . 17 ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 β†’ Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}))
95 ssun2 3299 . . . . . . . . . . . . . . . . . 18 {βŸ¨π‘§, π‘¦βŸ©} βŠ† (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})
96 vsnid 3624 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
9769dmsnop 5102 . . . . . . . . . . . . . . . . . . 19 dom {βŸ¨π‘§, π‘¦βŸ©} = {𝑧}
9896, 97eleqtrri 2253 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ dom {βŸ¨π‘§, π‘¦βŸ©}
99 funssfv 5541 . . . . . . . . . . . . . . . . . 18 ((Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∧ {βŸ¨π‘§, π‘¦βŸ©} βŠ† (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∧ 𝑧 ∈ dom {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10095, 98, 99mp3an23 1329 . . . . . . . . . . . . . . . . 17 (Fun (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10180, 94, 1003syl 17 . . . . . . . . . . . . . . . 16 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) = ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§))
10253, 69fvsn 5711 . . . . . . . . . . . . . . . 16 ({βŸ¨π‘§, π‘¦βŸ©}β€˜π‘§) = 𝑦
103101, 102eqtr2di 2227 . . . . . . . . . . . . . . 15 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§))
104 ralsnsg 3629 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V β†’ (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ [𝑧 / π‘₯]πœ‘))
10553, 104ax-mp 5 . . . . . . . . . . . . . . . 16 (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ [𝑧 / π‘₯]πœ‘)
106 elsni 3610 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ {𝑧} β†’ π‘₯ = 𝑧)
107106fveq2d 5519 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ {𝑧} β†’ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§))
108107eqeq2d 2189 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ {𝑧} β†’ (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) ↔ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§)))
109108biimparc 299 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) ∧ π‘₯ ∈ {𝑧}) β†’ 𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯))
110 sbceq1a 2972 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) β†’ (πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
111109, 110syl 14 . . . . . . . . . . . . . . . . 17 ((𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) ∧ π‘₯ ∈ {𝑧}) β†’ (πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
112111ralbidva 2473 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) β†’ (βˆ€π‘₯ ∈ {𝑧}πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
113105, 112bitr3id 194 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘§) β†’ ([𝑧 / π‘₯]πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
114103, 113syl 14 . . . . . . . . . . . . . 14 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ ([𝑧 / π‘₯]πœ‘ ↔ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
11593, 114mpbid 147 . . . . . . . . . . . . 13 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
116 ralun 3317 . . . . . . . . . . . . 13 ((βˆ€π‘₯ ∈ 𝑀 [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘ ∧ βˆ€π‘₯ ∈ {𝑧}[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘) β†’ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
11792, 115, 116syl2anc 411 . . . . . . . . . . . 12 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)
11853, 69opex 4229 . . . . . . . . . . . . . . 15 βŸ¨π‘§, π‘¦βŸ© ∈ V
119118snex 4185 . . . . . . . . . . . . . 14 {βŸ¨π‘§, π‘¦βŸ©} ∈ V
12019, 119unex 4441 . . . . . . . . . . . . 13 (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) ∈ V
121 feq1 5348 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ↔ (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡))
122 fveq1 5514 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (π‘”β€˜π‘₯) = ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯))
123122sbceq1d 2967 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ([(π‘”β€˜π‘₯) / 𝑦]πœ‘ ↔ [((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
124123ralbidv 2477 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘ ↔ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘))
125121, 124anbi12d 473 . . . . . . . . . . . . 13 (𝑔 = (𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}) β†’ ((𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘) ↔ ((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘)))
126120, 125spcev 2832 . . . . . . . . . . . 12 (((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©}):(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[((𝑓 βˆͺ {βŸ¨π‘§, π‘¦βŸ©})β€˜π‘₯) / 𝑦]πœ‘) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
12780, 117, 126syl2anc 411 . . . . . . . . . . 11 (((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) ∧ (𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))
128127ex 115 . . . . . . . . . 10 ((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) β†’ ((𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
129128exlimdv 1819 . . . . . . . . 9 ((Β¬ 𝑧 ∈ 𝑀 ∧ 𝑦 ∈ 𝐡 ∧ [𝑧 / π‘₯]πœ‘) β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))
1301293exp 1202 . . . . . . . 8 (Β¬ 𝑧 ∈ 𝑀 β†’ (𝑦 ∈ 𝐡 β†’ ([𝑧 / π‘₯]πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘)))))
13159, 67, 130rexlimd 2591 . . . . . . 7 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆƒπ‘¦ ∈ 𝐡 [𝑧 / π‘₯]πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
13258, 131syl5 32 . . . . . 6 (Β¬ 𝑧 ∈ 𝑀 β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ (βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“) β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
133132a2d 26 . . . . 5 (Β¬ 𝑧 ∈ 𝑀 β†’ ((βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
13449, 133syl5 32 . . . 4 (Β¬ 𝑧 ∈ 𝑀 β†’ ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
135134adantl 277 . . 3 ((𝑀 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑀) β†’ ((βˆ€π‘₯ ∈ 𝑀 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:π‘€βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑀 πœ“)) β†’ (βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘”(𝑔:(𝑀 βˆͺ {𝑧})⟢𝐡 ∧ βˆ€π‘₯ ∈ (𝑀 βˆͺ {𝑧})[(π‘”β€˜π‘₯) / 𝑦]πœ‘))))
1366, 12, 31, 37, 45, 135findcard2s 6889 . 2 (𝐴 ∈ Fin β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘ β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“)))
137136imp 124 1 ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘¦ ∈ 𝐡 πœ‘) β†’ βˆƒπ‘“(𝑓:𝐴⟢𝐡 ∧ βˆ€π‘₯ ∈ 𝐴 πœ“))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 978   = wceq 1353  βˆƒwex 1492   ∈ wcel 2148   β‰  wne 2347  βˆ€wral 2455  βˆƒwrex 2456  Vcvv 2737  [wsbc 2962   βˆͺ cun 3127   ∩ cin 3128   βŠ† wss 3129  βˆ…c0 3422  {csn 3592  βŸ¨cop 3595  dom cdm 4626  Fun wfun 5210  βŸΆwf 5212  β€“1-1-ontoβ†’wf1o 5215  β€˜cfv 5216  Fincfn 6739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-er 6534  df-en 6740  df-fin 6742
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator