tz7.49 - Metamath Proof Explorer

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

Theorem tz7.49 8374

Description: Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.)

**Hypotheses**
Ref	Expression
tz7.49.1	⊢ 𝐹 Fn On
tz7.49.2	⊢ (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))

**Assertion**
Ref	Expression
tz7.49	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐹,𝑦 𝜑,𝑦 Allowed substitution hints: 𝜑(𝑥) 𝐵(𝑥,𝑦)

Proof of Theorem tz7.49 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ne 2931	. . . . . . . . 9 ⊢ ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
2	1	ralbii 3080	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ ↔ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
3		tz7.49.2	. . . . . . . . 9 ⊢ (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
4		ralim 3074	. . . . . . . . 9 ⊢ (∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → (∀𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
5	3, 4	sylbi 217	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
6	2, 5	biimtrrid 243	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))))
7		tz7.49.1	. . . . . . . . 9 ⊢ 𝐹 Fn On
8	7	tz7.48-3 8373	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ 𝐴 ∈ V)
9		elex 3459	. . . . . . . 8 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
10	8, 9	nsyl3 138	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ¬ ∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))
11	6, 10	nsyli 157	. . . . . 6 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅))
12		dfrex2 3061	. . . . . 6 ⊢ (∃𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ↔ ¬ ∀𝑥 ∈ On ¬ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
13	11, 12	imbitrrdi 252	. . . . 5 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) = ∅))
14		imaeq2 6013	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦))
15	14	difeq2d 4076	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐴 ∖ (𝐹 “ 𝑥)) = (𝐴 ∖ (𝐹 “ 𝑦)))
16	15	eqeq1d 2736	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ↔ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
17	16	onminex 7745	. . . . 5 ⊢ (∃𝑥 ∈ On (𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
18	13, 17	syl6 35	. . . 4 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅)))
19		df-ne 2931	. . . . . . 7 ⊢ ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ↔ ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅)
20	19	ralbii 3080	. . . . . 6 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ↔ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅)
21	20	anbi2i 623	. . . . 5 ⊢ (((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ↔ ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
22	21	rexbii 3081	. . . 4 ⊢ (∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ↔ ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ (𝐴 ∖ (𝐹 “ 𝑦)) = ∅))
23	18, 22	imbitrrdi 252	. . 3 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)))
24		nfra1 3258	. . . . 5 ⊢ Ⅎ𝑥∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))
25	3, 24	nfxfr 1854	. . . 4 ⊢ Ⅎ𝑥𝜑
26		simpllr 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)
27		fnfun 6590	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn On → Fun 𝐹)
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ Fun 𝐹
29		fvelima 6897	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ (𝐹 “ 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑧)
30	28, 29	mpan 690	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝐹 “ 𝑥) → ∃𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑧)
31		nfv 1915	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝜑
32		nfra1 3258	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅
33	31, 32	nfan 1900	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)
34		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝑥 ∈ On → 𝑧 ∈ 𝐴)
35		rsp 3222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝑦 ∈ 𝑥 → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
36	35	adantld 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
37		onelon 6340	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
38	15	neeq1d 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑦 → ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ ↔ (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
39		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
40	39, 15	eleq12d 2828	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) ↔ (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦))))
41	38, 40	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑦 → (((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) ↔ ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
42	41	rspcv 3570	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On → (∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
43	3, 42	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (𝜑 → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
44	43	com23 86	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ On → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
45	37, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
46	36, 45	sylcom 30	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
47	46	com3r 87	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
48	47	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦))))
49	48	expcomd 416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑦 ∈ 𝑥 → (𝑥 ∈ On → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
50		eldifi 4081	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → (𝐹‘𝑦) ∈ 𝐴)
51		eleq1 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) = 𝑧 → ((𝐹‘𝑦) ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
52	50, 51	syl5ibcom 245	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → ((𝐹‘𝑦) = 𝑧 → 𝑧 ∈ 𝐴))
53	49, 52	syl8 76	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑦 ∈ 𝑥 → (𝑥 ∈ On → ((𝐹‘𝑦) = 𝑧 → 𝑧 ∈ 𝐴))))
54	53	com34 91	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑦 ∈ 𝑥 → ((𝐹‘𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧 ∈ 𝐴))))
55	33, 34, 54	rexlimd 3241	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (∃𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑧 → (𝑥 ∈ On → 𝑧 ∈ 𝐴)))
56	30, 55	syl5 34	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑧 ∈ (𝐹 “ 𝑥) → (𝑥 ∈ On → 𝑧 ∈ 𝐴)))
57	56	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑥 ∈ On → (𝑧 ∈ (𝐹 “ 𝑥) → 𝑧 ∈ 𝐴)))
58	57	imp 406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝑧 ∈ (𝐹 “ 𝑥) → 𝑧 ∈ 𝐴))
59	58	ssrdv 3937	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → (𝐹 “ 𝑥) ⊆ 𝐴)
60		ssdif0 4316	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ (𝐹 “ 𝑥) ↔ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅)
61	60	biimpri 228	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → 𝐴 ⊆ (𝐹 “ 𝑥))
62	59, 61	anim12i 613	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐹 “ 𝑥)))
63		eqss 3947	. . . . . . . . . 10 ⊢ ((𝐹 “ 𝑥) = 𝐴 ↔ ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐹 “ 𝑥)))
64	62, 63	sylibr 234	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → (𝐹 “ 𝑥) = 𝐴)
65		onss 7728	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ On → 𝑥 ⊆ On)
66	32, 31	nfan 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑)
67		nfv 1915	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦 𝑥 ⊆ On
68	66, 67	nfan 1900	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On)
69		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑧(((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦 ∈ 𝑥)
70		ssel 3925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → 𝑦 ∈ On))
71		onss 7728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
72	7	fndmi 6594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ dom 𝐹 = On
73	71, 72	sseqtrrdi 3973	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ On → 𝑦 ⊆ dom 𝐹)
74		funfvima2 7175	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun 𝐹 ∧ 𝑦 ⊆ dom 𝐹) → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹 “ 𝑦)))
75	28, 73, 74	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ On → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹 “ 𝑦)))
76	70, 75	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹 “ 𝑦))))
77	35	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅))
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅)))
79	70, 78, 44	syl10 79	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝜑 → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦))))))
80	79	imp4a 422	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)))))
81		eldifn 4082	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → ¬ (𝐹‘𝑦) ∈ (𝐹 “ 𝑦))
82		eleq1a 2829	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ((𝐹‘𝑦) = (𝐹‘𝑧) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑦)))
83	82	con3d 152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → (¬ (𝐹‘𝑦) ∈ (𝐹 “ 𝑦) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
84	81, 83	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑦) ∈ (𝐴 ∖ (𝐹 “ 𝑦)) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
85	80, 84	syl8 76	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
86	85	com34 91	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑦) → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
87	76, 86	syldd 72	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
88	87	com4r 94	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))))
89	88	imp31 417	. . . . . . . . . . . . . . . . . 18 ⊢ ((((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦 ∈ 𝑥) → (𝑧 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
90	69, 89	ralrimi 3232	. . . . . . . . . . . . . . . . 17 ⊢ ((((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) ∧ 𝑦 ∈ 𝑥) → ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧))
91	90	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → (𝑦 ∈ 𝑥 → ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
92	68, 91	ralrimi 3232	. . . . . . . . . . . . . . 15 ⊢ (((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) ∧ 𝑥 ⊆ On) → ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧))
93	92	ex 412	. . . . . . . . . . . . . 14 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧)))
94	93	ancld 550	. . . . . . . . . . . . 13 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ⊆ On → (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧))))
95	7	tz7.48lem 8370	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑦 ¬ (𝐹‘𝑦) = (𝐹‘𝑧)) → Fun ^◡(𝐹 ↾ 𝑥))
96	65, 94, 95	syl56 36	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ 𝜑) → (𝑥 ∈ On → Fun ^◡(𝐹 ↾ 𝑥)))
97	96	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (𝑥 ∈ On → Fun ^◡(𝐹 ↾ 𝑥)))
98	97	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) → Fun ^◡(𝐹 ↾ 𝑥))
99	98	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → Fun ^◡(𝐹 ↾ 𝑥))
100	26, 64, 99	3jca 1128	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) ∧ 𝑥 ∈ On) ∧ (𝐴 ∖ (𝐹 “ 𝑥)) = ∅) → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))
101	100	exp41 434	. . . . . . 7 ⊢ (𝜑 → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (𝑥 ∈ On → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))))
102	101	com23 86	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))))
103	102	com34 91	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ On → ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))))
104	103	imp4a 422	. . . 4 ⊢ (𝜑 → (𝑥 ∈ On → (((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))))
105	25, 104	reximdai 3236	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) = ∅ ∧ ∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))
106	23, 105	syld 47	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥))))
107	106	impcom 407	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ^◡(𝐹 ↾ 𝑥)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2930 ∀wral 3049 ∃wrex 3058 Vcvv 3438 ∖ cdif 3896 ⊆ wss 3899 ∅c0 4283 ^◡ccnv 5621 dom cdm 5622 ↾ cres 5624 “ cima 5625 Oncon0 6315 Fun wfun 6484 Fn wfn 6485 ‘cfv 6490

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pr 5375 ax-un 7678

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-ord 6318 df-on 6319 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498

This theorem is referenced by: tz7.49c 8375

W3C validator