fin1a2lem12 - Metamath Proof Explorer

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

Theorem fin1a2lem12 10519

Description: Lemma for fin1a2 10523. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)

**Assertion**
Ref	Expression
fin1a2lem12	⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Proof of Theorem fin1a2lem12 Dummy variables 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 490	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐵 ∈ Fin^III)
2		simpll1 1231	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ⊆ 𝒫 𝐵)
3	2	adantr 486	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → 𝐴 ⊆ 𝒫 𝐵)
4		ssrab2 4008	. . . . . . . 8 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐴
5	4	unissi 4879	. . . . . . 7 ⊢ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ ∪ 𝐴
6		sspwuni 5063	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
7	6	biimpi 219	. . . . . . 7 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ 𝐴 ⊆ 𝐵)
8	5, 7	sstrid 3924	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
9	3, 8	syl 18	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
10		elpw2g 5300	. . . . . 6 ⊢ (𝐵 ∈ Fin^III → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
11	10	ad2antlr 740	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
12	9, 11	mpbird 260	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵)
13	12	fmpttd 7142	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵)
14		vex 3458	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
15	14	sucex 7847	. . . . . . . . . 10 ⊢ suc 𝑑 ∈ V
16		sssucid 6466	. . . . . . . . . 10 ⊢ 𝑑 ⊆ suc 𝑑
17		ssdomg 9058	. . . . . . . . . 10 ⊢ (suc 𝑑 ∈ V → (𝑑 ⊆ suc 𝑑 → 𝑑 ≼ suc 𝑑))
18	15, 16, 17	mp2 9	. . . . . . . . 9 ⊢ 𝑑 ≼ suc 𝑑
19		domtr 9065	. . . . . . . . 9 ⊢ ((𝑓 ≼ 𝑑 ∧ 𝑑 ≼ suc 𝑑) → 𝑓 ≼ suc 𝑑)
20	18, 19	mpan2 704	. . . . . . . 8 ⊢ (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑)
21	20	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐴 → (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑))
22	21	ss2rabi 4004	. . . . . 6 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑}
23		uniss 4878	. . . . . 6 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
24	22, 23	mp1i 14	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
25		id 23	. . . . . 6 ⊢ (𝑑 ∈ ω → 𝑑 ∈ ω)
26		pwexg 5345	. . . . . . . . 9 ⊢ (𝐵 ∈ Fin^III → 𝒫 𝐵 ∈ V)
27	26	adantl 487	. . . . . . . 8 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝒫 𝐵 ∈ V)
28	27, 2	ssexd 5291	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ∈ V)
29		rabexg 5304	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
30		uniexg 7784	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
31	28, 29, 30	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
32		breq2 5110	. . . . . . . . 9 ⊢ (𝑒 = 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ 𝑑))
33	32	rabbidv 3423	. . . . . . . 8 ⊢ (𝑒 = 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
34	33	unieqd 4883	. . . . . . 7 ⊢ (𝑒 = 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
35		eqid 2763	. . . . . . 7 ⊢ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})
36	34, 35	fvmptg 7017	. . . . . 6 ⊢ ((𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
37	25, 31, 36	syl2anr 609	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
38		peano2 7928	. . . . . 6 ⊢ (𝑑 ∈ ω → suc 𝑑 ∈ ω)
39		rabexg 5304	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
40		uniexg 7784	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
41	28, 39, 40	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
42		breq2 5110	. . . . . . . . 9 ⊢ (𝑒 = suc 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ suc 𝑑))
43	42	rabbidv 3423	. . . . . . . 8 ⊢ (𝑒 = suc 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
44	43	unieqd 4883	. . . . . . 7 ⊢ (𝑒 = suc 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
45	44, 35	fvmptg 7017	. . . . . 6 ⊢ ((suc 𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
46	38, 41, 45	syl2anr 609	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
47	24, 37, 46	3sstr4d 3968	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
48	47	ralrimiva 3158	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
49		fin34i 10489	. . 3 ⊢ ((𝐵 ∈ Fin^III ∧ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵 ∧ ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑)) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
50	1, 13, 48, 49	syl3anc 1399	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
51		fin1a2lem11 10518	. . . . . 6 ⊢ (( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
52	51	adantrr 730	. . . . 5 ⊢ (( [⊊] Or 𝐴 ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
53	52	3ad2antl2 1205	. . . 4 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
54	53	adantr 486	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
55		simpll3 1233	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 ∈ 𝐴)
56		simplrr 790	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ≠ ∅)
57		sspwuni 5063	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 ⊆ ∅)
58		ss0b 4354	. . . . . . . . . . 11 ⊢ (∪ 𝐴 ⊆ ∅ ↔ ∪ 𝐴 = ∅)
59	57, 58	bitri 278	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 = ∅)
60		pw0 4833	. . . . . . . . . . . . 13 ⊢ 𝒫 ∅ = {∅}
61	60	sseq2i 3942	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ {∅})
62		sssn 4785	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
63	61, 62	bitri 278	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
64		df-ne 2960	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
65		0ex 5265	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
66	65	unisn 4889	. . . . . . . . . . . . . . . 16 ⊢ ∪ {∅} = ∅
67	65	snid 4623	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ {∅}
68	66, 67	eqeltri 2860	. . . . . . . . . . . . . . 15 ⊢ ∪ {∅} ∈ {∅}
69		unieq 4881	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → ∪ 𝐴 = ∪ {∅})
70		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → 𝐴 = {∅})
71	69, 70	eleq12d 2858	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = {∅} → (∪ 𝐴 ∈ 𝐴 ↔ ∪ {∅} ∈ {∅}))
72	68, 71	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝐴 = {∅} → ∪ 𝐴 ∈ 𝐴)
73	72	orim2i 924	. . . . . . . . . . . . 13 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 = ∅ ∨ ∪ 𝐴 ∈ 𝐴))
74	73	ord 878	. . . . . . . . . . . 12 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (¬ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
75	64, 74	biimtrid 245	. . . . . . . . . . 11 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
76	63, 75	sylbi 220	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
77	59, 76	sylbir 238	. . . . . . . . 9 ⊢ (∪ 𝐴 = ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
78	77	com12 33	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∪ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
79	78	con3d 153	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (¬ ∪ 𝐴 ∈ 𝐴 → ¬ ∪ 𝐴 = ∅))
80	56, 55, 79	sylc 66	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 = ∅)
81		ioran 999	. . . . . 6 ⊢ (¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅) ↔ (¬ ∪ 𝐴 ∈ 𝐴 ∧ ¬ ∪ 𝐴 = ∅))
82	55, 80, 81	sylanbrc 595	. . . . 5 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
83		uniun 4893	. . . . . . . 8 ⊢ ∪ (𝐴 ∪ {∅}) = (∪ 𝐴 ∪ ∪ {∅})
84	66	uneq2i 4167	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∪ {∅}) = (∪ 𝐴 ∪ ∅)
85		un0 4347	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∅) = ∪ 𝐴
86	83, 84, 85	3eqtri 2790	. . . . . . 7 ⊢ ∪ (𝐴 ∪ {∅}) = ∪ 𝐴
87	86	eleq1i 2855	. . . . . 6 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ ∪ 𝐴 ∈ (𝐴 ∪ {∅}))
88		elun 4155	. . . . . 6 ⊢ (∪ 𝐴 ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}))
89	65	elsn2 4626	. . . . . . 7 ⊢ (∪ 𝐴 ∈ {∅} ↔ ∪ 𝐴 = ∅)
90	89	orbi2i 926	. . . . . 6 ⊢ ((∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
91	87, 88, 90	3bitri 300	. . . . 5 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
92	82, 91	sylnibr 332	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}))
93		unieq 4881	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = ∪ (𝐴 ∪ {∅}))
94		id 23	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
95	93, 94	eleq12d 2858	. . . . 5 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
96	95	notbid 321	. . . 4 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
97	92, 96	syl5ibrcom 250	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})))
98	54, 97	mpd 16	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
99	50, 98	pm2.65da 829	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∪ cun 4152 ∅c0 4281 𝒫 cpw 4560 {csn 4588 ∪ cuni 4870 class class class wbr 5106 ↦ cmpt 5190 Or wor 5563 ran crn 5657 suc csuc 6385 ⟶wf 6557 ‘cfv 6561 [⊊] crpss 7765 ωcom 7904 ≼ cdom 9002 Fincfn 9004 Fin^IIIcfin3 10389

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-rpss 7766 df-om 7905 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-er 8748 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-wdom 9589 df-card 10050 df-fin4 10395 df-fin3 10396

This theorem is used by: fin1a2s 10522

W3C validator