MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ac6sfi Structured version   Visualization version   GIF version

Theorem ac6sfi 8156
Description: A version of ac6s 9258 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 3130 . . . 4 (𝑢 = ∅ → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑))
2 feq2 5989 . . . . . 6 (𝑢 = ∅ → (𝑓:𝑢𝐵𝑓:∅⟶𝐵))
3 raleq 3130 . . . . . 6 (𝑢 = ∅ → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓))
42, 3anbi12d 746 . . . . 5 (𝑢 = ∅ → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
54exbidv 1847 . . . 4 (𝑢 = ∅ → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
61, 5imbi12d 334 . . 3 (𝑢 = ∅ → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))))
7 raleq 3130 . . . 4 (𝑢 = 𝑤 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝑤𝑦𝐵 𝜑))
8 feq2 5989 . . . . . 6 (𝑢 = 𝑤 → (𝑓:𝑢𝐵𝑓:𝑤𝐵))
9 raleq 3130 . . . . . 6 (𝑢 = 𝑤 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝑤 𝜓))
108, 9anbi12d 746 . . . . 5 (𝑢 = 𝑤 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
1110exbidv 1847 . . . 4 (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
127, 11imbi12d 334 . . 3 (𝑢 = 𝑤 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓))))
13 raleq 3130 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑))
14 feq2 5989 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢𝐵𝑓:(𝑤 ∪ {𝑧})⟶𝐵))
15 raleq 3130 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))
1614, 15anbi12d 746 . . . . . 6 (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
1716exbidv 1847 . . . . 5 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
18 feq1 5988 . . . . . . 7 (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵𝑔:(𝑤 ∪ {𝑧})⟶𝐵))
19 fvex 6163 . . . . . . . . . 10 (𝑓𝑥) ∈ V
20 ac6sfi.1 . . . . . . . . . 10 (𝑦 = (𝑓𝑥) → (𝜑𝜓))
2119, 20sbcie 3456 . . . . . . . . 9 ([(𝑓𝑥) / 𝑦]𝜑𝜓)
22 fveq1 6152 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
2322sbceq1d 3426 . . . . . . . . 9 (𝑓 = 𝑔 → ([(𝑓𝑥) / 𝑦]𝜑[(𝑔𝑥) / 𝑦]𝜑))
2421, 23syl5bbr 274 . . . . . . . 8 (𝑓 = 𝑔 → (𝜓[(𝑔𝑥) / 𝑦]𝜑))
2524ralbidv 2981 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
2618, 25anbi12d 746 . . . . . 6 (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
2726cbvexv 2274 . . . . 5 (∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
2817, 27syl6bb 276 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
2913, 28imbi12d 334 . . 3 (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
30 raleq 3130 . . . 4 (𝑢 = 𝐴 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜑))
31 feq2 5989 . . . . . 6 (𝑢 = 𝐴 → (𝑓:𝑢𝐵𝑓:𝐴𝐵))
32 raleq 3130 . . . . . 6 (𝑢 = 𝐴 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝐴 𝜓))
3331, 32anbi12d 746 . . . . 5 (𝑢 = 𝐴 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3433exbidv 1847 . . . 4 (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3530, 34imbi12d 334 . . 3 (𝑢 = 𝐴 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))))
36 f0 6048 . . . 4 ∅:∅⟶𝐵
37 0ex 4755 . . . . 5 ∅ ∈ V
38 ral0 4053 . . . . . . 7 𝑥 ∈ ∅ 𝜓
3938biantru 526 . . . . . 6 (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
40 feq1 5988 . . . . . 6 (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔ ∅:∅⟶𝐵))
4139, 40syl5bbr 274 . . . . 5 (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵))
4237, 41spcev 3289 . . . 4 (∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
4336, 42mp1i 13 . . 3 (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
44 ssun1 3759 . . . . . . 7 𝑤 ⊆ (𝑤 ∪ {𝑧})
45 ssralv 3650 . . . . . . 7 (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑))
4644, 45ax-mp 5 . . . . . 6 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑)
4746imim1i 63 . . . . 5 ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
48 ssun2 3760 . . . . . . . . 9 {𝑧} ⊆ (𝑤 ∪ {𝑧})
49 ssralv 3650 . . . . . . . . 9 ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑))
5048, 49ax-mp 5 . . . . . . . 8 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑)
51 vex 3192 . . . . . . . . . 10 𝑧 ∈ V
52 ralsnsg 4192 . . . . . . . . . 10 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑))
5351, 52ax-mp 5 . . . . . . . . 9 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑)
54 sbcrex 3500 . . . . . . . . 9 ([𝑧 / 𝑥]𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5553, 54bitri 264 . . . . . . . 8 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5650, 55sylib 208 . . . . . . 7 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
57 nfv 1840 . . . . . . . 8 𝑦 ¬ 𝑧𝑤
58 nfv 1840 . . . . . . . . 9 𝑦𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)
59 nfv 1840 . . . . . . . . . . 11 𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵
60 nfcv 2761 . . . . . . . . . . . 12 𝑦(𝑤 ∪ {𝑧})
61 nfsbc1v 3441 . . . . . . . . . . . 12 𝑦[(𝑔𝑥) / 𝑦]𝜑
6260, 61nfral 2940 . . . . . . . . . . 11 𝑦𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑
6359, 62nfan 1825 . . . . . . . . . 10 𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6463nfex 2151 . . . . . . . . 9 𝑦𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6558, 64nfim 1822 . . . . . . . 8 𝑦(∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
66 simprl 793 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑓:𝑤𝐵)
67 vex 3192 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
6851, 67f1osn 6138 . . . . . . . . . . . . . . 15 {⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦}
69 f1of 6099 . . . . . . . . . . . . . . 15 ({⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦} → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
7068, 69mp1i 13 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
71 simpl2 1063 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦𝐵)
7271snssd 4314 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {𝑦} ⊆ 𝐵)
7370, 72fssd 6019 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵)
74 simpl1 1062 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ¬ 𝑧𝑤)
75 disjsn 4221 . . . . . . . . . . . . . 14 ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑤)
7674, 75sylibr 224 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅)
77 fun2 6029 . . . . . . . . . . . . 13 (((𝑓:𝑤𝐵 ∧ {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵) ∧ (𝑤 ∩ {𝑧}) = ∅) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
7866, 73, 76, 77syl21anc 1322 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
79 simprr 795 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 𝜓)
80 eleq1a 2693 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑤 → (𝑧 = 𝑥𝑧𝑤))
8180necon3bd 2804 . . . . . . . . . . . . . . . . . 18 (𝑥𝑤 → (¬ 𝑧𝑤𝑧𝑥))
8281impcom 446 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝑤𝑥𝑤) → 𝑧𝑥)
83 fvunsn 6405 . . . . . . . . . . . . . . . . 17 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥))
84 dfsbcq 3423 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → ([((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑[(𝑓𝑥) / 𝑦]𝜑))
8584, 21syl6rbb 277 . . . . . . . . . . . . . . . . 17 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
8682, 83, 853syl 18 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑤𝑥𝑤) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
8786ralbidva 2980 . . . . . . . . . . . . . . 15 𝑧𝑤 → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
8874, 87syl 17 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
8979, 88mpbid 222 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
90 simpl3 1064 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → [𝑧 / 𝑥]𝜑)
91 ffun 6010 . . . . . . . . . . . . . . . . 17 ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}))
92 ssun2 3760 . . . . . . . . . . . . . . . . . 18 {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩})
93 vsnid 4185 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
9467dmsnop 5573 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑧, 𝑦⟩} = {𝑧}
9593, 94eleqtrri 2697 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}
96 funssfv 6171 . . . . . . . . . . . . . . . . . 18 ((Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
9792, 95, 96mp3an23 1413 . . . . . . . . . . . . . . . . 17 (Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
9878, 91, 973syl 18 . . . . . . . . . . . . . . . 16 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
9951, 67fvsn 6406 . . . . . . . . . . . . . . . 16 ({⟨𝑧, 𝑦⟩}‘𝑧) = 𝑦
10098, 99syl6req 2672 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
101 ralsnsg 4192 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑))
10251, 101ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑)
103 elsni 4170 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
104103fveq2d 6157 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑧} → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
105104eqeq2d 2631 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧)))
106105biimparc 504 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
107 sbceq1a 3432 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
108106, 107syl 17 . . . . . . . . . . . . . . . . 17 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
109108ralbidva 2980 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
110102, 109syl5bbr 274 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
111100, 110syl 17 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
11290, 111mpbid 222 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
113 ralun 3778 . . . . . . . . . . . . 13 ((∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
11489, 112, 113syl2anc 692 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
115 vex 3192 . . . . . . . . . . . . . 14 𝑓 ∈ V
116 snex 4874 . . . . . . . . . . . . . 14 {⟨𝑧, 𝑦⟩} ∈ V
117115, 116unex 6916 . . . . . . . . . . . . 13 (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∈ V
118 feq1 5988 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵))
119 fveq1 6152 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
120119sbceq1d 3426 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ([(𝑔𝑥) / 𝑦]𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
121120ralbidv 2981 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
122118, 121anbi12d 746 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)))
123117, 122spcev 3289 . . . . . . . . . . . 12 (((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
12478, 114, 123syl2anc 692 . . . . . . . . . . 11 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
125124ex 450 . . . . . . . . . 10 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → ((𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
126125exlimdv 1858 . . . . . . . . 9 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
1271263exp 1261 . . . . . . . 8 𝑧𝑤 → (𝑦𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))))
12857, 65, 127rexlimd 3020 . . . . . . 7 𝑧𝑤 → (∃𝑦𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
12956, 128syl5 34 . . . . . 6 𝑧𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
130129a2d 29 . . . . 5 𝑧𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
13147, 130syl5 34 . . . 4 𝑧𝑤 → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
132131adantl 482 . . 3 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
1336, 12, 29, 35, 43, 132findcard2s 8153 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
134133imp 445 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3189  [wsbc 3421  cun 3557  cin 3558  wss 3559  c0 3896  {csn 4153  cop 4159  dom cdm 5079  Fun wfun 5846  wf 5848  1-1-ontowf1o 5851  cfv 5852  Fincfn 7907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-om 7020  df-1o 7512  df-er 7694  df-en 7908  df-fin 7911
This theorem is referenced by:  fissuni  8223  fipreima  8224  indexfi  8226  finacn  8825  axcc4dom  9215  ttukeylem6  9288  firest  16025  ablfaclem3  18418  ablfac2  18420  cmpcovf  21117  cmpsub  21126  tgcmp  21127  hauscmplem  21132  comppfsc  21258  ptcnplem  21347  alexsubALTlem3  21776  alexsubALT  21778  tsmsxplem1  21879  ovolicc2lem5  23212  ovolicc2  23213  limciun  23581  cvmliftlem15  31023  matunitlindflem2  33073  ptrecube  33076  istotbnd3  33237  sstotbnd2  33240  sstotbnd  33241  prdsbnd  33259  prdstotbnd  33260  heiborlem1  33277  heibor  33287  kelac1  37148  hbt  37216
  Copyright terms: Public domain W3C validator